//==============================================================================
//	
//	Copyright (c) 2002-
//	Authors:
//	* Andrew Hinton <ug60axh@cs.bham.ac.uk> (University of Birmingham)
//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
//	
//------------------------------------------------------------------------------
//	
//	This file is part of PRISM.
//	
//	PRISM is free software; you can redistribute it and/or modify
//	it under the terms of the GNU General Public License as published by
//	the Free Software Foundation; either version 2 of the License, or
//	(at your option) any later version.
//	
//	PRISM is distributed in the hope that it will be useful,
//	but WITHOUT ANY WARRANTY; without even the implied warranty of
//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
//	GNU General Public License for more details.
//	
//	You should have received a copy of the GNU General Public License
//	along with PRISM; if not, write to the Free Software Foundation,
//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
//	
//==============================================================================

package userinterface.model;

import java.util.*;
import java.awt.*;
import java.awt.event.*;
import javax.swing.*;
import javax.swing.tree.*;
import javax.swing.event.*;

import userinterface.*;
import userinterface.model.graphicModel.GUIGraphicModelEditor;
import userinterface.model.graphicModel.*;
import userinterface.model.computation.*;
import parser.ast.*;
import parser.type.*;
import prism.*;

public class GUIMultiModelTree extends JPanel implements MouseListener
{
    //Constants
    public static final int TREE_SYNCHRONIZED_GOOD = 0;
    public static final int TREE_SYNCHRONIZED_BAD = 1;
    public static final int TREE_NOT_SYNCHRONIZED = 2;
    
    //Attributes
    private GUIMultiModelHandler handler;
    private GUIGraphicModelEditor graphicEditor;
    private boolean editable;
    
    //Graphical elements
    private JTree tree;
    private JPopupMenu moduleCollectionPopup;
    private Action addModule;
    private JPopupMenu declarationCollectionPopup;
    private Action addBooleanGlobal, addIntegerGlobal;
    private JPopupMenu constantsCollectionPopup;
    private Action addBooleanConstant, addDoubleConstant, addIntegerConstant;
    private JPopupMenu modulePopup;
    private Action renameModule, removeModule, addBoolean, addInteger;
    private JPopupMenu declarationPopup;
    private Action renameDeclaration, removeDeclaration;
    private JPopupMenu expressionPopup;
    private Action editExpression;
    private JPopupMenu modelTypePopup;
    private JRadioButton non, pro, sto;
    
    //Tree listener
    private EventListenerList listenerList = new EventListenerList();
    
    //Tree nodes
    private DefaultTreeModel theModel;
    private ModelRootNode root;
    private ModelTypeNode modelType;
    private ModuleCollectionNode modules;
    private DeclarationCollectionNode declarations;
    private ConstantCollectionNode constants;
    
    private ArrayList editableModules;
    private ArrayList editableDeclarations;
    private ArrayList editableConstants;
    
    private ImageIcon animIcon;
    private boolean isParsing;
    private IconThread parseThread;
    
    private PrismTreeNode lastPopNode;
    
    //State
    private int parseSynchState;
    
    public GUIMultiModelTree(GUIMultiModelHandler handler, boolean editable)
    {
        this.handler = handler;
        this.editable = editable;
        graphicEditor = null;
        root = new ModelRootNode();
        theModel = new DefaultTreeModel(root);
        newTree(editable);
        initComponents();
        animIcon = GUIPrism.getIconFromImage("smallClockAnim1.png");
        isParsing = false;
        tree.addMouseListener(this);
        
        tree.setEditable(true);
        
        JTextArea area = new JTextArea();
        ToolTipManager.sharedInstance().registerComponent(tree);
    }
    
    public GUIMultiModelTree(GUIMultiModelHandler handler)
    {
        this(handler, false);
    }
    
    static int modCounter = 1;
    public void a_addModule()
    {
        ModuleNode newNode = new ModuleNode("newModule"+modCounter, true);
        try
        {
            newNode.addVariable(new StateVarNode(newNode));
        }
        catch(prism.PrismException e)
        {
            //canny get here
        }
        editableModules.add(newNode);
        modules.addModule(newNode);
        int index = modules.getIndex(newNode);
        theModel.nodesWereInserted(modules, new int[]
        {index});
        modCounter++;
        if(this.graphicEditor != null) graphicEditor.addNewModule(newNode);
        if(graphicEditor != null) graphicEditor.setModified();
        
    }
    
    public ModuleNode a_requestNewModule(String name)
    {
        ModuleNode newNode = new ModuleNode(name, true);
        try
        {
            newNode.addVariable(new StateVarNode(newNode));
        }
        catch(prism.PrismException e)
        {
            //canny get here
        }
        editableModules.add(newNode);
        modules.addModule(newNode);
        int index = modules.getIndex(newNode);
        theModel.nodesWereInserted(modules, new int[]
        {index});
        modCounter++;
        if(this.graphicEditor != null) graphicEditor.addNewModule(newNode);
        if(graphicEditor != null) graphicEditor.setModified();
        return newNode;
    }
    
    static int globCounter = 1;
    public void a_addIntegerGlobal()
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            
            GlobalNode newNode = new GlobalNode("g"+globCounter, init, min, max, true);
            editableDeclarations.add(newNode);
            declarations.addDeclaration(newNode);
            int index = declarations.getIndex(newNode);
            theModel.nodesWereInserted(declarations, new int[]
            {index});
            globCounter++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
            //This should never happen
        }
        
        handler.hasModified(true);
    }
    
    public void a_addIntegerGlobal(String name, String mins, String maxs, String inits) throws PrismException
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits);
            Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(mins);
            Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(maxs);
            
            GlobalNode newNode = new GlobalNode(name, init, min, max, true);
            editableDeclarations.add(newNode);
            declarations.addDeclaration(newNode);
            int index = declarations.getIndex(newNode);
            theModel.nodesWereInserted(declarations, new int[]
            {index});
            globCounter++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Global integer "+name+" has invalid parameter");
        }
        
        handler.hasModified(true);
    }
    
    public void a_addBooleanGlobal()
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false");
            
            GlobalBoolNode newNode = new GlobalBoolNode("g"+globCounter, init, true);
            editableDeclarations.add(newNode);
            declarations.addDeclaration(newNode);
            int index = declarations.getIndex(newNode);
            theModel.nodesWereInserted(declarations, new int[]
            {index});
            globCounter++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
            //This should never happen
        }
        handler.hasModified(true);
    }
    
    public void a_addBooleanGlobal(String name, String inits) throws PrismException
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(inits);
            
            GlobalBoolNode newNode = new GlobalBoolNode(name, init, true);
            editableDeclarations.add(newNode);
            declarations.addDeclaration(newNode);
            int index = declarations.getIndex(newNode);
            theModel.nodesWereInserted(declarations, new int[]
            {index});
            globCounter++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Global boolean "+name+" has invalid parameter");
        }
        handler.hasModified(true);
    }
    
    static int consCount = 1;
    public void a_addIntegerConstant()
    {
        try
        {
            Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            IntegerConstantNode newNode = new IntegerConstantNode("c"+consCount, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
        }
        handler.hasModified(true);
    }
    
    public void a_addIntegerConstant(String name, String val) throws PrismException
    {
        try
        {
            Expression value;
            if(val == null)
                value = null;
            else
                value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val);
            IntegerConstantNode newNode = new IntegerConstantNode(name, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Constant integer "+name+" has invalid parameter");
        }
        handler.hasModified(true);
    }
    
    public void a_addBooleanConstant()
    {
        try
        {
            Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false");
            BoolConstantNode newNode = new BoolConstantNode("c"+consCount, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
        }
        handler.hasModified(true);
    }
    
    public void a_addBooleanConstant(String name, String val) throws PrismException
    {
        try
        {
            Expression value;
            if(val == null)
                value = null;
            else
                value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val);
            BoolConstantNode newNode = new BoolConstantNode(name, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Constant boolean "+name+" has invalid parameter");
        }
        handler.hasModified(true);
    }
    
    public void a_addDoubleConstant()
    {
        try
        {
            Expression value = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0.0");
            DoubleConstantNode newNode = new DoubleConstantNode("c"+consCount, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
        }
        handler.hasModified(true);
    }
    
    public void a_addDoubleConstant(String name, String val) throws PrismException
    {
        try
        {
            Expression value;
            if(val == null)
                value = null;
            else
                value = handler.getGUIPlugin().getPrism().parseSingleExpressionString(val);
            DoubleConstantNode newNode = new DoubleConstantNode(name, value, true);
            editableConstants.add(newNode);
            constants.addConstant(newNode);
            int index = constants.getIndex(newNode);
            theModel.nodesWereInserted(constants, new int[]
            {index});
            consCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Constant double "+name+" has invalid parameter");
        }
        handler.hasModified(true);
    }
    
    public void a_removeModule(ModuleNode m)
    {
        int index = modules.getIndex(m);
        editableModules.remove(m);
        modules.remove(m);
        theModel.nodesWereRemoved(modules, new int[]
        {index}, new Object[]
        {m});
        if(graphicEditor != null) graphicEditor.removeModule(m);
        else
        {
            //System.out.println("graphic editor is null");
        }
        if(graphicEditor != null) graphicEditor.setModified();
        else
        {
            //System.out.println("graphic editor is null");
        }
        handler.hasModified(true);
    }
    
    public void a_renameModule(ModuleNode m)
    {
        
        String s = JOptionPane.showInputDialog("New module name:", m.getName());
        if(s == null) return;
        
        try
        {
            Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s);
            if(exp instanceof ExpressionIdent)
            {
                m.setName(s);
                theModel.nodeChanged(m);
                theModel.nodeStructureChanged(m);
                if(this.graphicEditor != null)
                {
                    graphicEditor.notifyChangeTo(m);
                }
            }
            else
            {
                handler.getGUIPlugin().error("Invalid module name");
            }
        }
        catch(PrismException exx)
        {
            handler.getGUIPlugin().error("Invalid module name");
        }
        
        
        
        handler.hasModified(true);
    }
    
    public void a_renameDeclaration(DeclarationNode d)
    {
        String type = "";
        if(d instanceof BoolNode || d instanceof VarNode)
            type = " variable";
        else if(d instanceof GlobalNode || d instanceof GlobalBoolNode)
            type = " global";
        else if(d instanceof ConstantNode)
            type = " constant";
        
        String s = JOptionPane.showInputDialog("New"+type+" name:", d.getName());
        if(s == null) return;
        
        try
        {
            Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s);
            if(exp instanceof ExpressionIdent)
            {
                d.setName(s);
                theModel.nodeChanged(d);
                theModel.nodeStructureChanged(d);
            }
            else
            {
                handler.getGUIPlugin().error("Invalid declaration name");
            }
        }
        catch(PrismException exx)
        {
            handler.getGUIPlugin().error("Invalid module name");
        }
        
        
        handler.hasModified(true);
    }
    
    public void a_removeVariable(DeclarationNode d, ModuleNode m)
    {
        int index = m.getIndex(d);
        m.remove(d);
        theModel.nodesWereRemoved(m, new int[]
        {index}, new Object[]
        {d});
        if(graphicEditor != null) graphicEditor.setModified();
        handler.hasModified(true);
    }
    
    public void a_removeGlobal(DeclarationNode d)
    {
        int index = declarations.getIndex(d);
        editableDeclarations.remove(d);
        declarations.remove(d);
        theModel.nodesWereRemoved(declarations, new int[]
        {index}, new Object[]
        {d});
        if(graphicEditor != null) graphicEditor.setModified();
        handler.hasModified(true);
    }
    
    public void a_removeConstant(ConstantNode c)
    {
        int index = constants.getIndex(c);
        editableConstants.remove(c);
        constants.remove(c);
        theModel.nodesWereRemoved(constants, new int[]
        {index}, new Object[]
        {c});
        if(graphicEditor != null) graphicEditor.setModified();
        handler.hasModified(true);
    }
    
    
    public void a_addLocalBoolean(ModuleNode m, LoadGraphicModelThread.BooleanVariable var) throws PrismException
    {
        try
        {
            Expression init;
            if(var != null)
                init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init);
            else init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false");
            
            BoolNode newNode = new BoolNode(var.name,  init, true);
            m.add(newNode);
            int index = m.getIndex(newNode);
            theModel.nodesWereInserted(m, new int[]
            {index});
            varCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Local boolean "+var.name+" has an invalid parameter");
        }
        handler.hasModified(true);
    }
    
    static int varCount = 1;
    public void a_addLocalBoolean(ModuleNode m)
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("false");
            
            BoolNode newNode = new BoolNode("v"+varCount,  init, true);
            m.add(newNode);
            int index = m.getIndex(newNode);
            theModel.nodesWereInserted(m, new int[]
            {index});
            varCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
            //This should never happen
        }
        handler.hasModified(true);
    }
    
    public void a_addLocalInteger(ModuleNode m, LoadGraphicModelThread.IntegerVariable var) throws PrismException
    {
        try
        {
            Expression init;
            if(var.init == null)
                init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            else
                init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.init);
            Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.min);
            Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(var.max);
            
            VarNode newNode = new VarNode(var.name, init, min, max, true);
            m.addVariable(newNode);
            int index = m.getIndex(newNode);
            theModel.nodesWereInserted(m, new int[]
            {index});
            varCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            throw new PrismException("Local integer "+var.name+" has an invalid parameter");
        }
        handler.hasModified(true);
    }
    
    public void a_addLocalInteger(ModuleNode m)
    {
        try
        {
            Expression init = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            Expression min = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            Expression max = handler.getGUIPlugin().getPrism().parseSingleExpressionString("0");
            
            VarNode newNode = new VarNode("v"+varCount, init, min, max, true);
            m.addVariable(newNode);
            int index = m.getIndex(newNode);
            theModel.nodesWereInserted(m, new int[]
            {index});
            varCount++;
            if(graphicEditor != null) graphicEditor.setModified();
        }
        catch(Exception e)
        {
            System.err.println("UNEXPECTED ERROR: "+e.getMessage());
            e.printStackTrace();
            //This should never happen
        }
        handler.hasModified(true);
    }
    
    public void a_editExpression(ExpressionNode en)
    {
        String defa;
        if(en.getValue() == null) defa = "?";
        else defa = en.getValue().toString();
        String s = JOptionPane.showInputDialog("New Expression:", defa);
        if(s == null) return;
        try
        {
            if(s.equals(""))
            {
                en.setValue(null);
            }
            else
            {
                Expression exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(s);
                en.setValue(exp);
            }
            theModel.nodeChanged(en);
        }
        catch(Exception e)
        {
            handler.getGUIPlugin().error("Syntax error in expression:\n"+s);
        }
        
        handler.hasModified(true);
    }
    
    public void a_setModelType(ModelType type)
    {
    	modelType.setModelType(type);
        handler.hasModified(true);
    }
    
    public int getParseSynchState()
    {
        return parseSynchState;
    }
    
    public void setGraphicModelEditor(GUIGraphicModelEditor graphicEditor)
    {
        this.graphicEditor = graphicEditor;
    }
    
    public void startParsing()
    {
        isParsing = true;
        if(parseThread != null) parseThread.interrupt();
        parseThread = new IconThread(0);
        parseThread.start();
    }
    
    public void stopParsing()
    {
        isParsing = false;
        if(parseThread != null) parseThread.interrupt();
        tree.repaint();
    }
    
    public void newTree()
    { this.newTree(false); }
    
    public void newTree(boolean editable)
    {
        this.editable = editable;
        root.removeAllChildren();
        parseSynchState = TREE_NOT_SYNCHRONIZED;
        {
            root.setUserObject("Model: " + handler.getShortActiveFileName());
            modelType = new ModelTypeNode("<Unknown>", editable);
            root.add(modelType);
            if(editable)
            {
                modules = new GUIMultiModelTree.ModuleCollectionNode();
                declarations = new GUIMultiModelTree.DeclarationCollectionNode();
                constants = new GUIMultiModelTree.ConstantCollectionNode();
                root.add(modules);
                root.add(declarations);
                root.add(constants);
                theModel.nodeStructureChanged(root);
            }
            else
            {
                modules = new ModuleCollectionNode();
                declarations = new DeclarationCollectionNode();
                constants = new ConstantCollectionNode();
                theModel.nodeStructureChanged(root);
            }
        }
        editableModules = new ArrayList();
        editableDeclarations = new ArrayList();
        editableConstants = new ArrayList();
        
        modCounter = 1;
    }
    
    public void update(ModulesFile parsedModel)
    {
        parseSynchState = (parsedModel==null) ? TREE_NOT_SYNCHRONIZED : TREE_SYNCHRONIZED_GOOD;
        if(editable) updateEditable(parsedModel);
        else updateUnEditable(parsedModel);
    }
    
    private void updateUnEditable(ModulesFile parsedModel)
    {
        String fn = handler.getShortActiveFileName();
        if(!root.getUserObject().equals(fn))
        {
            root.setUserObject("Model: " + fn);
            theModel.nodeChanged(root);
        }
        
        if(parsedModel != null)
        {
            String tp = parsedModel.getTypeString();
            if(!modelType.getValue().equals(tp))
            {
                modelType.setUserObject(tp);
                theModel.nodeChanged(modelType);
            }
            
            //MODULES
            
            //If there is no module tree, but we need to have modules, add the tre
            if(root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0)
            {
                root.add(modules);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(modules)});
            }
            //If there is a module tree, but no modules, remove the module tree
            else if(root.getIndex(modules) != -1 && parsedModel.getNumModules() == 0)
            {
                int index = root.getIndex(modules);
                root.remove(modules);
                theModel.nodesWereRemoved(root, new int[]
                {index}, new Object[]
                {modules});
            }
            
                        /*  Create 2 ArrayLists.  One of Modules in the tree and one of modules
                         *  not in the tree. */
            ArrayList inTree = new ArrayList();
            ArrayList notInTree = new ArrayList();
            
            for(int i = 0; i < parsedModel.getNumModules(); i++)
            {
                Module aMod = parsedModel.getModule(i);
                if(moduleIsMember(aMod)) inTree.add(aMod);
                else notInTree.add(aMod);
            }
            
            //make sure modules in the tree are valid
            for(int i = 0; i < inTree.size(); i++)
            {
                Module inTreeMod = (Module)inTree.get(i);
                int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1
                ModuleNode inTreeNode = (ModuleNode)modules.getChildAt(treeIndex);
                
                                /*  Check its variables getting variables which are already there
                                 *  and putting them in varInTree, and getting variables which
                                 *  are not there and putting them in varNotInTree*/
                ArrayList varInTree = new ArrayList();
                ArrayList varNotInTree = new ArrayList();
                
                for(int j = 0; j < inTreeMod.getNumDeclarations(); j++)
                {
                    Declaration d = inTreeMod.getDeclaration(j);
                    if(variableIsMember(d, inTreeNode)) varInTree.add(d);
                    else varNotInTree.add(d);
                }
                
                //make sure variables in this module tree are valid
                for(int j = 0; j < varInTree.size(); j++)
                {
                    Declaration inTreeDec = (Declaration)varInTree.get(j);
                    int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode);
                    DeclarationNode dNode = (DeclarationNode)inTreeNode.getChildAt(decIndex);
                    if(dNode instanceof VarNode)
                    {
                        VarNode vNode = (VarNode)dNode;
                        DeclarationInt dt = (DeclarationInt)inTreeDec.getDeclType();
                        vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                        vNode.setMin(dt.getLow());
                        vNode.setMax(dt.getHigh());
                        theModel.nodesChanged(vNode, new int []
                        {0,1,2});
                    }
                    else if(dNode instanceof BoolNode)
                    {
                        BoolNode bNode = (BoolNode)dNode;
                        bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                        theModel.nodesChanged(bNode, new int[]
                        {0});
                    }
                    
                }
                //add variable in varNotInTree to the tree
                int[] cIndices = new int[varNotInTree.size()];
                for(int j = 0; j < varNotInTree.size(); j++)
                {
                    Declaration notTreeDec = (Declaration)varNotInTree.get(j);
                    if(notTreeDec.getType() instanceof TypeInt)
                    {
                    	DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType();
                        VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                        inTreeNode.add(newVariable);
                        cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
                    }
                    else if(notTreeDec.getType() instanceof TypeBool)
                    {
                        BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false);
                        inTreeNode.add(newVariable);
                        cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
                    }
                }
                theModel.nodesWereInserted(inTreeNode, cIndices);
                
                                /*  remove variables which are in the tree but not in varInTree or
                                 *  varNotInTree */
                ArrayList removeNodes = new ArrayList();
                for(int j = 0; j < inTreeNode.getChildCount(); j++)
                {
                    DeclarationNode vNode = (DeclarationNode)inTreeNode.getChildAt(j);
                    if(!variableExists(vNode, varInTree, varNotInTree))
                    {
                        removeNodes.add(vNode);
                    }
                }
                Object[] remObj = new Object[removeNodes.size()];
                int[] remInd = new int[removeNodes.size()];
                for(int j = 0; j < removeNodes.size(); j++)
                {
                    DeclarationNode vNode = (DeclarationNode)removeNodes.get(j);
                    int index = inTreeNode.getIndex(vNode);
                    remObj[j] = vNode;
                    remInd[j] = index;
                }
                //remove nodes backwards
                for(int j =removeNodes.size()-1; j >= 0; j--)
                {
                    inTreeNode.remove(remInd[j]);
                }
                theModel.nodesWereRemoved(inTreeNode, remInd, remObj);
            }
            
            //add modules which are not in the tree
            for(int i = 0; i < notInTree.size(); i++)
            {
                Module aMod = (Module)notInTree.get(i);
                ModuleNode newNode = new ModuleNode(aMod.getName(),false);
                //add variables to this
                for(int j = 0; j < aMod.getNumDeclarations(); j++)
                {
                    Declaration aDec = aMod.getDeclaration(j);
                    
                    if(aDec.getType() instanceof TypeInt)
                    {
                    	DeclarationInt declInt = (DeclarationInt)aDec.getDeclType();
                        VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                        newNode.add(newVariable);
                    }
                    else if(aDec.getType() instanceof TypeBool)
                    {
                        BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false);
                        newNode.add(newVariable);
                    }
                }
                modules.addModule(newNode);
                int index = modules.getIndex(newNode);
                theModel.nodesWereInserted(modules, new int[]
                {index});
            }
            //remove modules from the tree which are not in either inTree or notInTree
            ArrayList removeNodes = new ArrayList();
            for(int i = 0; i < modules.getChildCount(); i++)
            {
                ModuleNode mNode = (ModuleNode)modules.getChildAt(i);
                if(!moduleExists(mNode, inTree, notInTree))
                {
                    removeNodes.add(mNode);
                }
            }
            Object[] remObj = new Object[removeNodes.size()];
            int[] remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                ModuleNode mNode = (ModuleNode)removeNodes.get(i);
                int index = modules.getIndex(mNode);
                remObj[i] = mNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                modules.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(modules, remInd, remObj);
            
            //DECLARATIONS
            
            //If there is no declaration tree, but we need to have declarations, add the tre
            if(root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0)
            {
                root.add(declarations);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(declarations)});
            }
            //If there is a module tree, but no modules, remove the module tree
            else if(root.getIndex(declarations) != -1 && parsedModel.getNumGlobals() == 0)
            {
                int index = root.getIndex(declarations);
                root.remove(declarations);
                theModel.nodesWereRemoved(root, new int[]
                {index}, new Object[]
                {declarations});
            }
            
                        /*  Create 2 ArrayLists.  One of Declarations in the tree and one of declarations
                         *  not in the tree. */
            ArrayList decInTree = new ArrayList();
            ArrayList decNotInTree = new ArrayList();
            
            for(int i = 0; i < parsedModel.getNumGlobals(); i++)
            {
                Declaration d = parsedModel.getGlobal(i);
                if(declarationIsMember(d)) decInTree.add(d);
                else decNotInTree.add(d);
            }
            //make sure declarations in this declaration tree are valid
            for(int i = 0; i < decInTree.size(); i++)
            {
                Declaration inTreeDec = (Declaration)decInTree.get(i);
                int decIndex = getIndexOfDec(inTreeDec);
                DeclarationNode dNode = (DeclarationNode)declarations.getChildAt(decIndex);
                if(dNode instanceof GlobalNode)
                {
                    GlobalNode vNode = (GlobalNode)declarations.getChildAt(decIndex);
                	DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType();
                    vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                    vNode.setMin(declInt.getLow());
                    vNode.setMax(declInt.getHigh());
                    theModel.nodesChanged(vNode, new int []
                    {0,1,2});
                }
                else if(dNode instanceof BoolNode)
                {
                    BoolNode bNode = (BoolNode)dNode;
                    bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                    theModel.nodesChanged(bNode, new int[]
                    {0});
                }
                
            }
            
            //add declarations in decNotInTree to the tree
            int[] cIndices = new int[decNotInTree.size()];
            for(int i = 0; i < decNotInTree.size(); i++)
            {
                Declaration notTreeDec = (Declaration)decNotInTree.get(i);
                if(notTreeDec.getType() instanceof TypeInt)
                {
                	DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType();
                    GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                    declarations.add(newVariable);
                    cIndices[i] = getIndexOfDec(notTreeDec);
                }
                else if(notTreeDec.getType() instanceof TypeBool)
                {
                    BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false);
                    declarations.add(newVariable);
                    cIndices[i] = getIndexOfDec(notTreeDec);
                }
            }
            theModel.nodesWereInserted(declarations, cIndices);
            
            
                        /*  remove declarations which are in the tree but not in decInTree or
                         *  decNotInTree */
            removeNodes = new ArrayList();
            for(int i = 0; i < declarations.getChildCount(); i++)
            {
                DeclarationNode vNode = (DeclarationNode)declarations.getChildAt(i);
                if(!declarationExists(vNode, decInTree, decNotInTree))
                {
                    removeNodes.add(vNode);
                }
            }
            remObj = new Object[removeNodes.size()];
            remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                DeclarationNode vNode = (DeclarationNode)removeNodes.get(i);
                int index = declarations.getIndex(vNode);
                remObj[i] = vNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                declarations.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(declarations, remInd, remObj);
            
            
            
            
            
            
            
            //CONSTANTS
            
            ConstantList csts = parsedModel.getConstantList();
            //If there is no constant tree, but we need to have constant, add the tre
            if(root.getIndex(constants) == -1 && csts.size() > 0)
            {
                root.add(constants);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(constants)});
            }
            //If there is a constant tree, but no constants, remove the module tree
            else if(root.getIndex(constants) != -1 && csts.size() == 0)
            {
                int index = root.getIndex(constants);
                root.remove(constants);
                theModel.nodesWereRemoved(root, new int[]
                {index}, new Object[]
                {constants});
            }
            
                        /*  Create 2 ArrayLists.  One of Constants in the tree and one of constants
                         *  not in the tree. */
            ArrayList conInTree = new ArrayList();
            ArrayList conNotInTree = new ArrayList();
            
            for(int i = 0; i < csts.size(); i++)
            {
                String name = csts.getConstantName(i);
                Expression expr = csts.getConstant(i);
                Type type = csts.getConstantType(i);
                ConstantNode cn;
                if (type instanceof TypeBool) {
                    cn = new BoolConstantNode(name, expr, false);
                } else if (type instanceof TypeDouble) {
                    cn = new DoubleConstantNode(name, expr, false);
                } else {
                    cn = new IntegerConstantNode(name, expr, false);
                }
                if(constantIsMember(cn)) conInTree.add(cn);
                else conNotInTree.add(cn);
            }
            
            //make sure constants in this declaration tree are valid
            for(int i = 0; i < conInTree.size(); i++)
            {
                ConstantNode inTreeCon = (ConstantNode)conInTree.get(i);
                int conIndex = getIndexOfCon(inTreeCon);
                ConstantNode cNode = (ConstantNode)constants.getChildAt(conIndex);
                if(cNode instanceof IntegerConstantNode)
                {
                    IntegerConstantNode iNode = (IntegerConstantNode)cNode;
                    
                    iNode.setName(inTreeCon.getName());
                    iNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(iNode, new int []
                    {0});
                }
                else if(cNode instanceof BoolConstantNode)
                {
                    BoolConstantNode bNode = (BoolConstantNode)cNode;
                    
                    bNode.setName(inTreeCon.getName());
                    bNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(bNode, new int []
                    {0});
                }
                else if(cNode instanceof DoubleConstantNode)
                {
                    DoubleConstantNode dNode = (DoubleConstantNode)cNode;
                    
                    dNode.setName(inTreeCon.getName());
                    dNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(dNode, new int []
                    {0});
                }
                
            }
            
            //add declarations in decNotInTree to the tree
            cIndices = new int[conNotInTree.size()];
            for(int i = 0; i < conNotInTree.size(); i++)
            {
                ConstantNode notTreeCon = (ConstantNode)conNotInTree.get(i);
                constants.add(notTreeCon);
                cIndices[i] = getIndexOfCon(notTreeCon);
            }
            theModel.nodesWereInserted(constants, cIndices);
            
            
                        /*  remove declarations which are in the tree but not in decInTree or
                         *  decNotInTree */
            removeNodes = new ArrayList();
            for(int i = 0; i < constants.getChildCount(); i++)
            {
                ConstantNode cNode = (ConstantNode)constants.getChildAt(i);
                if(!constantExists(cNode, conInTree, conNotInTree))
                {
                    removeNodes.add(cNode);
                }
            }
            remObj = new Object[removeNodes.size()];
            remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                ConstantNode vNode = (ConstantNode)removeNodes.get(i);
                int index = constants.getIndex(vNode);
                remObj[i] = vNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                constants.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(constants, remInd, remObj);
            
        }
        else
        {
            String tp = "<Unknown>";
            if(!modelType.getValue().equals(tp))
            {
                modelType.setUserObject(tp);
                theModel.nodeChanged(modelType);
            }
        }
        
        if(tree !=null) tree.repaint();
    }
    
    public boolean moduleExists(ModuleNode mNode, ArrayList inTree, ArrayList outTree)
    {
        for(int i = 0; i < inTree.size(); i++)
        {
            Module m = (Module)inTree.get(i);
            if(mNode.getName().equals(m.getName()))
            {
                return true;
            }
        }
        for(int i = 0; i < outTree.size(); i++)
        {
            Module m = (Module)outTree.get(i);
            if(mNode.getName().equals(m.getName()))
            {
                return true;
            }
        }
        return false;
    }
    public boolean variableExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree)
    {
        for(int i = 0; i < inTree.size(); i++)
        {
            Declaration d = (Declaration)inTree.get(i);
            if(vNode.getName().equals(d.getName()))
            {
                return true;
            }
        }
        for(int i = 0; i < outTree.size(); i++)
        {
            Declaration d = (Declaration)outTree.get(i);
            if(vNode.getName().equals(d.getName()))
            {
                return true;
            }
        }
        return false;
    }
    
    public boolean declarationExists(DeclarationNode vNode, ArrayList inTree, ArrayList outTree)
    {
        for(int i = 0; i < inTree.size(); i++)
        {
            Declaration d = (Declaration)inTree.get(i);
            if(vNode.getName().equals(d.getName()))
            {
                return true;
            }
        }
        for(int i = 0; i < outTree.size(); i++)
        {
            Declaration d = (Declaration)outTree.get(i);
            if(vNode.getName().equals(d.getName()))
            {
                return true;
            }
        }
        return false;
    }
    
    public boolean constantExists(ConstantNode cNode, ArrayList inTree, ArrayList outTree)
    {
        for(int i = 0; i < inTree.size(); i++)
        {
            ConstantNode c = (ConstantNode)inTree.get(i);
            if(c.equals(cNode)) return true;
        }
        
        for(int i = 0; i < outTree.size(); i++)
        {
            ConstantNode c = (ConstantNode)outTree.get(i);
            if(c.equals(cNode)) return true;
        }
        return false;
    }
    
    
    public boolean moduleIsMember(Module aMod)
    {
        boolean member = false;
        for(int i = 0; i < modules.getChildCount(); i++)
        {
            ModuleNode node = (ModuleNode)modules.getChildAt(i);
            if(node.getName().equals(aMod.getName()))
            {
                member = true;
                break;
            }
        }
        return member;
    }
    
    public boolean declarationIsMember(Declaration d)
    {
        boolean member = false;
        for(int i = 0; i < declarations.getChildCount(); i++)
        {
            DeclarationNode dec = (DeclarationNode)declarations.getChildAt(i);
            if(dec.getName().equals(d.getName())) //check same name
            {
                if(dec instanceof GlobalBoolNode && d.getType() instanceof TypeBool) //check type equality
                {
                    member = true;
                    break;
                }
                if(dec instanceof GlobalNode && d.getType() instanceof TypeInt)
                {
                    member = true;
                    break;
                }
            }
        }
        return member;
    }
    
    public boolean constantIsMember(ConstantNode n)
    {
        boolean member = false;
        for(int i = 0; i < constants.getChildCount(); i++)
        {
            ConstantNode inC = (ConstantNode)constants.getChildAt(i);
            if(inC.equals(n))
            {
                member = true;
                break;
            }
        }
        return member;
    }
    
    public boolean variableIsMember(Declaration d, ModuleNode node)
    {
        boolean member = false;
        for(int i = 0; i < node.getChildCount(); i++)
        {
            DeclarationNode dec = (DeclarationNode)node.getChildAt(i);
            if(dec.getName().equals(d.getName())) //check same name
            {
                if(dec instanceof BoolNode && d.getType() instanceof TypeBool) //check type equality
                {
                    member = true;
                    break;
                }
                if(dec instanceof VarNode && d.getType() instanceof TypeInt)
                {
                    member = true;
                    break;
                }
            }
        }
        return member;
    }
    
    public int getVarTreeIndexOf(Declaration d, ModuleNode node)
    {
        int member = -1;
        for(int i = 0; i < node.getChildCount(); i++)
        {
            DeclarationNode vNode = (DeclarationNode)node.getChildAt(i);
            if(vNode.getName().equals(d.getName()))
            {
                member = i;
                break;
            }
        }
        return member;
    }
    
    public int getModuleTreeIndexOf(Module aMod)
    {
        int member = -1;
        for(int i = 0; i < modules.getChildCount(); i++)
        {
            ModuleNode node = (ModuleNode)modules.getChildAt(i);
            if(node.getName().equals(aMod.getName()))
            {
                member = i;
                break;
            }
        }
        return member;
    }
    
    public int getIndexOfDec(Declaration d)
    {
        int member = -1;
        for(int i = 0; i < declarations.getChildCount(); i++)
        {
            DeclarationNode dec = (DeclarationNode)declarations.getChildAt(i);
            if(dec.getName().equals(d.getName()))
            {
                member = i;
                break;
            }
        }
        return member;
    }
    
    public int getIndexOfCon(ConstantNode cn)
    {
        int member = -1;
        
        for(int i = 0; i < constants.getChildCount(); i++)
        {
            ConstantNode cc = (ConstantNode)constants.getChildAt(i);
            if(cc.equals(cn))
            {
                member = i;
                break;
            }
        }
        return member;
    }
    
    private void updateEditable(ModulesFile parsedModel)
    {
        String fn = handler.getShortActiveFileName();
        if(!root.getUserObject().equals(fn))
        {
            root.setUserObject("Model: " + fn);
            theModel.nodeChanged(root);
        }
        
        if(parsedModel != null)
        {
            if(!modelType.getValue().equals(parsedModel.getType().toString()))
            {
                modelType.setModelType(parsedModel.getModelType());
            }
            
            //MODULES
            
            //If there is no module tree, but we need to have modules, add the tre
            if(root.getIndex(modules) == -1 && parsedModel.getNumModules() > 0)
            {
                root.add(modules);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(modules)});
            }
            
            
                        /*  Create 2 ArrayLists.  One of Modules in the tree and one of modules
                         *  not in the tree. */
            ArrayList inTree = new ArrayList();
            ArrayList notInTree = new ArrayList();
            
            for(int i = 0; i < parsedModel.getNumModules(); i++)
            {
                Module aMod = parsedModel.getModule(i);
                if(moduleIsMember(aMod)) inTree.add(aMod);
                else notInTree.add(aMod);
            }
            
            //make sure modules in the tree are valid
            for(int i = 0; i < inTree.size(); i++)
            {
                Module inTreeMod = (Module)inTree.get(i);
                int treeIndex = getModuleTreeIndexOf(inTreeMod); //should not be -1
                ModuleNode inTreeNode = (ModuleNode)modules.getChildAt(treeIndex);
                
                                /*  Check its variables getting variables which are already there
                                 *  and putting them in varInTree, and getting variables which
                                 *  are not there and putting them in varNotInTree*/
                ArrayList varInTree = new ArrayList();
                ArrayList varNotInTree = new ArrayList();
                
                for(int j = 0; j < inTreeMod.getNumDeclarations(); j++)
                {
                    Declaration d = inTreeMod.getDeclaration(j);
                    if(variableIsMember(d, inTreeNode)) varInTree.add(d);
                    else varNotInTree.add(d);
                }
                
                //make sure variables in this module tree are valid
                for(int j = 0; j < varInTree.size(); j++)
                {
                    Declaration inTreeDec = (Declaration)varInTree.get(j);
                    int decIndex = getVarTreeIndexOf(inTreeDec, inTreeNode);
                    DeclarationNode dNode = (DeclarationNode)inTreeNode.getChildAt(decIndex);
                    if(dNode instanceof VarNode)
                    {
                        VarNode vNode = (VarNode)dNode;
                    	DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType();
                        vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                        vNode.setMin(declInt.getLow());
                        vNode.setMax(declInt.getHigh());
                        theModel.nodesChanged(vNode, new int []
                        {0,1,2});
                    }
                    else if(dNode instanceof BoolNode)
                    {
                        BoolNode bNode = (BoolNode)dNode;
                        bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                        theModel.nodesChanged(bNode, new int[]
                        {0});
                    }
                    
                }
                //add variable in varNotInTree to the tree
                int[] cIndices = new int[varNotInTree.size()];
                for(int j = 0; j < varNotInTree.size(); j++)
                {
                    Declaration notTreeDec = (Declaration)varNotInTree.get(j);
                    if(notTreeDec.getType() instanceof TypeInt)
                    {
                    	DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType();
                        VarNode newVariable = new VarNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                        inTreeNode.add(newVariable);
                        cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
                    }
                    else if(notTreeDec.getType() instanceof TypeBool)
                    {
                        BoolNode newVariable = new BoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false);
                        inTreeNode.add(newVariable);
                        cIndices[j] = getVarTreeIndexOf(notTreeDec, inTreeNode);
                    }
                }
                theModel.nodesWereInserted(inTreeNode, cIndices);
                
                                /*  remove variables which are in the tree but not in varInTree or
                                 *  varNotInTree */
                ArrayList removeNodes = new ArrayList();
                for(int j = 0; j < inTreeNode.getChildCount(); j++)
                {
                    DeclarationNode vNode = (DeclarationNode)inTreeNode.getChildAt(j);
                    if(!variableExists(vNode, varInTree, varNotInTree))
                    {
                        removeNodes.add(vNode);
                    }
                }
                Object[] remObj = new Object[removeNodes.size()];
                int[] remInd = new int[removeNodes.size()];
                for(int j = 0; j < removeNodes.size(); j++)
                {
                    DeclarationNode vNode = (DeclarationNode)removeNodes.get(j);
                    int index = inTreeNode.getIndex(vNode);
                    remObj[j] = vNode;
                    remInd[j] = index;
                }
                //remove nodes backwards
                for(int j =removeNodes.size()-1; j >= 0; j--)
                {
                    inTreeNode.remove(remInd[j]);
                }
                theModel.nodesWereRemoved(inTreeNode, remInd, remObj);
            }
            
            //add modules which are not in the tree
            for(int i = 0; i < notInTree.size(); i++)
            {
                Module aMod = (Module)notInTree.get(i);
                ModuleNode newNode = new ModuleNode(aMod.getName(),false);
                //add variables to this
                for(int j = 0; j < aMod.getNumDeclarations(); j++)
                {
                    Declaration aDec = aMod.getDeclaration(j);
                    
                    if(aDec.getType() instanceof TypeInt)
                    {
                    	DeclarationInt declInt = (DeclarationInt)aDec.getDeclType();
                        VarNode newVariable = new VarNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                        newNode.add(newVariable);
                    }
                    else if(aDec.getType() instanceof TypeBool)
                    {
                        BoolNode newVariable = new BoolNode(aDec.getName(), parsedModel.getSystemDefn() == null ? aDec.getStartOrDefault() : null, false);
                        newNode.add(newVariable);
                    }
                }
                modules.addModule(newNode);
                int index = modules.getIndex(newNode);
                theModel.nodesWereInserted(modules, new int[]
                {index});
            }
            //remove modules from the tree which are not in either inTree or notInTree
            ArrayList removeNodes = new ArrayList();
            for(int i = 0; i < modules.getChildCount(); i++)
            {
                ModuleNode mNode = (ModuleNode)modules.getChildAt(i);
                if(!mNode.isEditable() && !moduleExists(mNode, inTree, notInTree))
                {
                    removeNodes.add(mNode);
                }
            }
            Object[] remObj = new Object[removeNodes.size()];
            int[] remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                ModuleNode mNode = (ModuleNode)removeNodes.get(i);
                int index = modules.getIndex(mNode);
                remObj[i] = mNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                modules.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(modules, remInd, remObj);
            
            //DECLARATIONS
            
            //If there is no declaration tree, but we need to have declarations, add the tre
            if(root.getIndex(declarations) == -1 && parsedModel.getNumGlobals() > 0)
            {
                root.add(declarations);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(declarations)});
            }
            
                        /*  Create 2 ArrayLists.  One of Declarations in the tree and one of declarations
                         *  not in the tree. */
            ArrayList decInTree = new ArrayList();
            ArrayList decNotInTree = new ArrayList();
            
            for(int i = 0; i < parsedModel.getNumGlobals(); i++)
            {
                Declaration d = parsedModel.getGlobal(i);
                if(declarationIsMember(d)) decInTree.add(d);
                else decNotInTree.add(d);
            }
            
            //make sure declarations in this declaration tree are valid
            for(int i = 0; i < decInTree.size(); i++)
            {
                Declaration inTreeDec = (Declaration)decInTree.get(i);
                int decIndex = getIndexOfDec(inTreeDec);
                DeclarationNode dNode = (DeclarationNode)declarations.getChildAt(decIndex);
                if(dNode instanceof GlobalNode)
                {
                    GlobalNode vNode = (GlobalNode)declarations.getChildAt(decIndex);
                	DeclarationInt declInt = (DeclarationInt)inTreeDec.getDeclType();
                    vNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                    vNode.setMin(declInt.getLow());
                    vNode.setMax(declInt.getHigh());
                    theModel.nodesChanged(vNode, new int []
                    {0,1,2});
                }
                else if(dNode instanceof GlobalBoolNode)
                {
                    GlobalBoolNode bNode = (GlobalBoolNode)dNode;
                    bNode.setInitial(parsedModel.getSystemDefn() == null ? inTreeDec.getStartOrDefault() : null);
                    theModel.nodesChanged(bNode, new int[]
                    {0});
                }
                
            }
            
            //add declarations in decNotInTree to the tree
            int[] cIndices = new int[decNotInTree.size()];
            for(int i = 0; i < decNotInTree.size(); i++)
            {
                Declaration notTreeDec = (Declaration)decNotInTree.get(i);
                if(notTreeDec.getType() instanceof TypeInt)
                {
                	DeclarationInt declInt = (DeclarationInt)notTreeDec.getDeclType();
                    GlobalNode newVariable = new GlobalNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, declInt.getLow(), declInt.getHigh(), false);
                    declarations.add(newVariable);
                    cIndices[i] = getIndexOfDec(notTreeDec);
                }
                else if(notTreeDec.getType() instanceof TypeBool)
                {
                    GlobalBoolNode newVariable = new GlobalBoolNode(notTreeDec.getName(), parsedModel.getSystemDefn() == null ? notTreeDec.getStartOrDefault() : null, false);
                    declarations.add(newVariable);
                    cIndices[i] = getIndexOfDec(notTreeDec);
                }
            }
            theModel.nodesWereInserted(declarations, cIndices);
            
            
                        /*  remove declarations which are in the tree but not in decInTree or
                         *  decNotInTree */
            removeNodes = new ArrayList();
            for(int i = 0; i < declarations.getChildCount(); i++)
            {
                DeclarationNode vNode = (DeclarationNode)declarations.getChildAt(i);
                if(!vNode.isEditable() && !declarationExists(vNode, decInTree, decNotInTree))
                {
                    removeNodes.add(vNode);
                }
            }
            remObj = new Object[removeNodes.size()];
            remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                DeclarationNode vNode = (DeclarationNode)removeNodes.get(i);
                int index = declarations.getIndex(vNode);
                remObj[i] = vNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                declarations.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(declarations, remInd, remObj);
            
            
            
            
            
            
            
            //CONSTANTS
            
            ConstantList csts = parsedModel.getConstantList();
            //If there is no constant tree, but we need to have constant, add the tre
            if(root.getIndex(constants) == -1 && csts.size() > 0)
            {
                root.add(constants);
                theModel.nodesWereInserted(root, new int[]
                {root.getIndex(constants)});
            }
            
                        /*  Create 2 ArrayLists.  One of Constants in the tree and one of constants
                         *  not in the tree. */
            ArrayList conInTree = new ArrayList();
            ArrayList conNotInTree = new ArrayList();
            
            for(int i = 0; i < csts.size(); i++)
            {
                String name = csts.getConstantName(i);
                Expression expr = csts.getConstant(i);
                Type type = csts.getConstantType(i);
                ConstantNode cn;
                if (type instanceof TypeBool) {
                    cn = new BoolConstantNode(name, expr, false);
                } else if (type instanceof TypeDouble) {
                    cn = new DoubleConstantNode(name, expr, false);
                } else {
                    cn = new IntegerConstantNode(name, expr, false);
                }
                if(constantIsMember(cn)) conInTree.add(cn);
                else conNotInTree.add(cn);
            }
            
            //make sure constants in this declaration tree are valid
            for(int i = 0; i < conInTree.size(); i++)
            {
                ConstantNode inTreeCon = (ConstantNode)conInTree.get(i);
                int conIndex = getIndexOfCon(inTreeCon);
                ConstantNode cNode = (ConstantNode)constants.getChildAt(conIndex);
                if(cNode instanceof IntegerConstantNode)
                {
                    IntegerConstantNode iNode = (IntegerConstantNode)cNode;
                    
                    iNode.setName(inTreeCon.getName());
                    iNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(iNode, new int []
                    {0});
                }
                else if(cNode instanceof BoolConstantNode)
                {
                    BoolConstantNode bNode = (BoolConstantNode)cNode;
                    
                    bNode.setName(inTreeCon.getName());
                    bNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(bNode, new int []
                    {0});
                }
                else if(cNode instanceof DoubleConstantNode)
                {
                    DoubleConstantNode dNode = (DoubleConstantNode)cNode;
                    
                    dNode.setName(inTreeCon.getName());
                    dNode.setValue(inTreeCon.getValue());
                    theModel.nodesChanged(dNode, new int []
                    {0});
                }
                
            }
            
            //add declarations in decNotInTree to the tree
            cIndices = new int[conNotInTree.size()];
            for(int i = 0; i < conNotInTree.size(); i++)
            {
                ConstantNode notTreeCon = (ConstantNode)conNotInTree.get(i);
                constants.add(notTreeCon);
                cIndices[i] = getIndexOfCon(notTreeCon);
            }
            theModel.nodesWereInserted(constants, cIndices);
            
            
                        /*  remove declarations which are in the tree but not in decInTree or
                         *  decNotInTree */
            removeNodes = new ArrayList();
            for(int i = 0; i < constants.getChildCount(); i++)
            {
                ConstantNode cNode = (ConstantNode)constants.getChildAt(i);
                if(!cNode.isEditable() && !constantExists(cNode, conInTree, conNotInTree))
                {
                    removeNodes.add(cNode);
                }
            }
            remObj = new Object[removeNodes.size()];
            remInd = new int[removeNodes.size()];
            for(int i = 0; i < removeNodes.size(); i++)
            {
                ConstantNode vNode = (ConstantNode)removeNodes.get(i);
                int index = constants.getIndex(vNode);
                remObj[i] = vNode;
                remInd[i] = index;
            }
            //remove nodes backwards
            for(int i =removeNodes.size()-1; i >= 0; i--)
            {
                constants.remove(remInd[i]);
            }
            theModel.nodesWereRemoved(constants, remInd, remObj);
            
        }
        else
        {
                        /*String tp = "<Unknown>";
                        if(!modelType.getValue().equals(tp))
                        {
                                modelType.setUserObject(tp);
                                theModel.nodeChanged(modelType);
                        }*/
        }
        
        if(tree != null) tree.repaint();
    }
    
    public void lastParseFailed()
    {
        parseSynchState = TREE_SYNCHRONIZED_BAD;
        tree.repaint();
    }
    
    public void makeNotUpToDate()
    {
        parseSynchState = TREE_NOT_SYNCHRONIZED;
        tree.repaint();
    }
    
    private void initComponents()
    {
        tree = new JTree(theModel)
        {
            public String getToolTipText(MouseEvent event)
            {
                String ret = null;
                TreePath selectedPath = tree.getPathForLocation(event.getX(), event.getY());
                if(selectedPath != null)
                {
                    //if(selectedPath.getLastPathComponent() instanceof ModelRootNode)
                    if(parseSynchState == TREE_SYNCHRONIZED_BAD) return handler.getParseErrorMessage();
                    else if(parseSynchState == TREE_SYNCHRONIZED_GOOD) return "Model parsed successfully";
                    else return "Model not parsed";
                }
                
                return ret;
            }
            
            public boolean isPathEditable(TreePath path)
            {
                Object c = path.getLastPathComponent();
                if(c instanceof ValueNode)
                {
                    ValueNode v = (ValueNode)c;
                    return v.isEditable();
                }
                return false;
            }
            
        };
        PrismNodeRenderer prnr = new PrismNodeRenderer();
        tree.setCellRenderer(prnr);
                /*JComboBox typeCombo = new JComboBox(new Object[]
                {"Probabilistic", "Non-deterministic", "Stochastic"});
                typeCombo.setFont(tree.getFont());
                typeCombo.setBackground(tree.getBackground());
                ValueNodeCellEditor cellEdit = new ValueNodeCellEditor(new JTextField(), typeCombo);
                tree.setCellEditor(new DefaultTreeCellEditor(tree, prnr, cellEdit));*/
        tree.setEditable(true);
        tree.setCellEditor(new GUIMultiModelTree.ModelTreeCellEditor(tree, prnr));
        
        setLayout(new BorderLayout());
        JScrollPane scr = new JScrollPane();
        scr.setViewportView(tree);
        add(scr, BorderLayout.CENTER);
        
        moduleCollectionPopup = new JPopupMenu();
        addModule = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addModule();
            }
        };
        addModule.putValue(Action.LONG_DESCRIPTION, "Adds an editable module to the tree");
        addModule.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_A));
        addModule.putValue(Action.NAME, "Add Module");
        moduleCollectionPopup.add(addModule);
        
        declarationCollectionPopup = new JPopupMenu();
        addIntegerGlobal = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addIntegerGlobal();
            }
        };
        addIntegerGlobal.putValue(Action.NAME, "Add Global Integer");
        addBooleanGlobal = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addBooleanGlobal();
            }
        };
        addBooleanGlobal.putValue(Action.NAME, "Add Global Boolean");
        declarationCollectionPopup.add(addIntegerGlobal);
        declarationCollectionPopup.add(addBooleanGlobal);
        
        constantsCollectionPopup = new JPopupMenu();
        addIntegerConstant = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addIntegerConstant();
            }
        };
        addIntegerConstant.putValue(Action.NAME, "Add Integer Constant");
        addBooleanConstant = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addBooleanConstant();
            }
        };
        addBooleanConstant.putValue(Action.NAME, "Add Boolean Constant");
        addDoubleConstant = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                a_addDoubleConstant();
            }
        };
        addDoubleConstant.putValue(Action.NAME, "Add Double Constant");
        constantsCollectionPopup.add(addIntegerConstant);
        constantsCollectionPopup.add(addBooleanConstant);
        constantsCollectionPopup.add(addDoubleConstant);
        
        modulePopup = new JPopupMenu();
        removeModule = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null && lastPopNode instanceof ModuleNode)
                {
                    a_removeModule((ModuleNode)lastPopNode);
                    lastPopNode = null;
                }
            }
        };
        removeModule.putValue(Action.NAME, "Remove");
        addBoolean = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null && lastPopNode instanceof ModuleNode)
                {
                    a_addLocalBoolean((ModuleNode)lastPopNode);
                    lastPopNode = null;
                }
                
            }
        };
        addBoolean.putValue(Action.NAME, "Add Boolean Variable");
        addInteger = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null && lastPopNode instanceof ModuleNode)
                {
                    a_addLocalInteger((ModuleNode)lastPopNode);
                    lastPopNode = null;
                }
            }
        };
        addInteger.putValue(Action.NAME, "Add Integer Variable");
        renameModule = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null && lastPopNode instanceof ModuleNode)
                {
                    a_renameModule((ModuleNode)lastPopNode);
                    lastPopNode = null;
                }
            }
        };
        renameModule.putValue(Action.NAME, "Rename");
        modulePopup.add(renameModule);
        modulePopup.add(removeModule);
        //modulePopup.add(new JSplitter());
        modulePopup.add(addInteger);
        modulePopup.add(addBoolean);
        
        declarationPopup = new JPopupMenu();
        removeDeclaration = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null)
                {
                    if(lastPopNode instanceof BoolNode || lastPopNode instanceof VarNode)
                    {
                        ModuleNode m = whichModule((DeclarationNode)lastPopNode);
                        if(m != null) a_removeVariable((DeclarationNode)lastPopNode, m);
                    }
                    else if(lastPopNode instanceof GlobalNode || lastPopNode instanceof GlobalBoolNode)
                    {
                        a_removeGlobal((DeclarationNode)lastPopNode);
                    }
                    else if(lastPopNode instanceof ConstantNode)
                    {
                        a_removeConstant((ConstantNode)lastPopNode);
                    }
                }
            }
        };
        removeDeclaration.putValue(Action.NAME, "Remove");
        declarationPopup.add(removeDeclaration);
        
        renameDeclaration = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode != null)
                {
                    a_renameDeclaration((DeclarationNode)lastPopNode);
                }
            }
        };
        renameDeclaration.putValue(Action.NAME, "Rename");
        declarationPopup.add(renameDeclaration);
        
        expressionPopup = new JPopupMenu();
        
        editExpression = new AbstractAction()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(lastPopNode !=null)
                {
                    a_editExpression((ExpressionNode)lastPopNode);
                }
            }
        };
        editExpression.putValue(Action.NAME, "Edit");
        expressionPopup.add(editExpression);
        
        
        modelTypePopup = new JPopupMenu();
        
        non = new JRadioButton("Non-deterministic (mdp)");
        pro = new JRadioButton("Probabilistic (dtmc)");
        sto = new JRadioButton("Stochastic (ctmc)");
        
        ButtonGroup gro = new ButtonGroup();
        gro.add(non);
        gro.add(pro);
        gro.add(sto);
        
        non.setSelected(true);
        
        modelTypePopup.add(non);
        modelTypePopup.add(pro);
        modelTypePopup.add(sto);
        
        non.addActionListener(new ActionListener()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(non.isSelected())a_setModelType(ModelType.MDP);
                modelTypePopup.setVisible(false);
            }
        });
        
        pro.addActionListener(new ActionListener()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(pro.isSelected())a_setModelType(ModelType.DTMC);
                modelTypePopup.setVisible(false);
            }
        });
        
        sto.addActionListener(new ActionListener()
        {
            public void actionPerformed(ActionEvent e)
            {
                if(sto.isSelected())a_setModelType(ModelType.CTMC);
                modelTypePopup.setVisible(false);
            }
        });
    }
    
    public ModuleNode whichModule(DeclarationNode isIt)
    {
        for(int i = 0; i < editableModules.size(); i++)
        {
            ModuleNode mod = (ModuleNode)editableModules.get(i);
            int index = mod.getIndex(isIt);
            if(index > -1)
            {
                return mod;
            }
        }
        return null;
    }
    
    
    public void mouseClicked(MouseEvent e)
    {
    }
    
    public void mouseEntered(MouseEvent e)
    {
    }
    
    public void mouseExited(MouseEvent e)
    {
    }
    
    public void mousePressed(MouseEvent e)
    {
        if(e.isPopupTrigger())
        {
            lastPopNode = null;
            //root popup
            if(tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath())))
            {
                tree.setSelectionPath(new TreePath(root.getPath()));
                //now the root is selected, show the popup
                //(diabled for now)
                //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY());
            }
            //model type node
            if(editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath())))
            {
                tree.setSelectionPath(new TreePath(modelType.getPath()));
                modelTypePopup.show(tree,e.getX(), e.getY());
            }
            //module collection popup
            else if(editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath())))
            {
                tree.setSelectionPath(new TreePath(modules.getPath()));
                moduleCollectionPopup.show(tree,e.getX(),e.getY());
            }
            //declaration collection popup
            else if(editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath())))
            {
                tree.setSelectionPath(new TreePath(declarations.getPath()));
                declarationCollectionPopup.show(tree,e.getX(),e.getY());
            }
            else if(editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node
            {
                tree.setSelectionPath(new TreePath(constants.getPath()));
                constantsCollectionPopup.show(tree,e.getX(), e.getY());
            }
            else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode
            {
                TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY());
                for(int i = 0; i < editableModules.size(); i++) //search each module
                {
                    ModuleNode mn = (ModuleNode)editableModules.get(i);
                    if(new TreePath(mn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(mn.isEditable())
                        {
                            modulePopup.show(tree, e.getX(), e.getY());
                            lastPopNode = mn;
                            
                            if(graphicEditor != null)graphicEditor.switchModuleView(mn);
                        }
                        return;
                    }
                    for(int j = 0; j < mn.getChildCount(); j++)//search local variables
                    {
                        DeclarationNode dn = (DeclarationNode)mn.getChildAt(j);
                        if(new TreePath(dn.getPath()).equals(selectedPath))
                        {
                            tree.setSelectionPath(selectedPath);
                            if(dn.isEditable())
                            {
                                declarationPopup.show(tree, e.getX(), e.getY());
                                lastPopNode = dn;
                            }
                            return;
                        }
                    }
                }
                for(int i = 0; i < editableDeclarations.size(); i++)//search globals
                {
                    DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i);
                    if(new TreePath(dn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(dn.isEditable())
                        {
                            declarationPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = dn;
                        }
                        return;
                    }
                }
                for(int i = 0; i < editableConstants.size(); i++)//search constants
                {
                    DeclarationNode dn = (DeclarationNode)editableConstants.get(i);
                    if(new TreePath(dn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(dn.isEditable())
                        {
                            declarationPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = dn;
                        }
                        return;
                    }
                }
                
                //Could be an ExpressionNode
                if(tree.getSelectionPath() != null)
                {
                    TreeNode selectedNode = (TreeNode)tree.getSelectionPath().getLastPathComponent();
                    if(selectedNode instanceof ExpressionNode)
                    {
                        ExpressionNode en = (ExpressionNode)selectedNode;
                        if(en.isEditable())
                        {
                            expressionPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = en;
                        }
                    }
                }
                
            }
            
        }
        else
        {
            TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY());
            for(int i = 0; i < editableModules.size(); i++) //search each module
            {
                ModuleNode mn = (ModuleNode)editableModules.get(i);
                if(new TreePath(mn.getPath()).equals(selectedPath))
                {
                    tree.setSelectionPath(selectedPath);
                    if(graphicEditor != null)graphicEditor.switchModuleView(mn);
                    return;
                }
            }
        }
        
    }
    
    public void mouseReleased(MouseEvent e)
    {
        if(e.isPopupTrigger())
        {
            lastPopNode = null;
            //root popup
            if(tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(root.getPath())))
            {
                tree.setSelectionPath(new TreePath(root.getPath()));
                //now the root is selected, show the popup
                //(diabled for now)
                //((GUIMultiModel)(handler.getGUIPlugin())).getPopup().show(tree, e.getX(), e.getY());
            }
            //model type node
            if(editable && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modelType.getPath())))
            {
                tree.setSelectionPath(new TreePath(modelType.getPath()));
                modelTypePopup.show(tree,e.getX(), e.getY());
            }
            //module collection popup
            else if(editable && modules != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(modules.getPath())))
            {
                tree.setSelectionPath(new TreePath(modules.getPath()));
                moduleCollectionPopup.show(tree,e.getX(),e.getY());
            }
            //declaration collection popup
            else if(editable && declarations != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(declarations.getPath())))
            {
                tree.setSelectionPath(new TreePath(declarations.getPath()));
                declarationCollectionPopup.show(tree,e.getX(),e.getY());
            }
            else if(editable && constants != null && tree.getClosestPathForLocation(e.getX(), e.getY()).equals(new TreePath(constants.getPath())))//constant collection node
            {
                tree.setSelectionPath(new TreePath(constants.getPath()));
                constantsCollectionPopup.show(tree,e.getX(), e.getY());
            }
            else // is the path on a ModuleNode or a DeclarationNode or an ExpressionNode
            {
                TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY());
                for(int i = 0; i < editableModules.size(); i++) //search each module
                {
                    ModuleNode mn = (ModuleNode)editableModules.get(i);
                    if(new TreePath(mn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(mn.isEditable())
                        {
                            modulePopup.show(tree, e.getX(), e.getY());
                            lastPopNode = mn;
                            
                            if(graphicEditor != null)graphicEditor.switchModuleView(mn);
                        }
                        return;
                    }
                    for(int j = 0; j < mn.getChildCount(); j++)//search local variables
                    {
                        DeclarationNode dn = (DeclarationNode)mn.getChildAt(j);
                        if(new TreePath(dn.getPath()).equals(selectedPath))
                        {
                            tree.setSelectionPath(selectedPath);
                            if(dn.isEditable())
                            {
                                declarationPopup.show(tree, e.getX(), e.getY());
                                lastPopNode = dn;
                            }
                            return;
                        }
                    }
                }
                for(int i = 0; i < editableDeclarations.size(); i++)//search globals
                {
                    DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i);
                    if(new TreePath(dn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(dn.isEditable())
                        {
                            declarationPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = dn;
                        }
                        return;
                    }
                }
                for(int i = 0; i < editableConstants.size(); i++)//search constants
                {
                    DeclarationNode dn = (DeclarationNode)editableConstants.get(i);
                    if(new TreePath(dn.getPath()).equals(selectedPath))
                    {
                        tree.setSelectionPath(selectedPath);
                        if(dn.isEditable())
                        {
                            declarationPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = dn;
                        }
                        return;
                    }
                }
                
                //Could be an ExpressionNode
                if(tree.getSelectionPath() != null)
                {
                    TreeNode selectedNode = (TreeNode)tree.getSelectionPath().getLastPathComponent();
                    if(selectedNode instanceof ExpressionNode)
                    {
                        ExpressionNode en = (ExpressionNode)selectedNode;
                        if(en.isEditable())
                        {
                            expressionPopup.show(tree, e.getX(), e.getY());
                            lastPopNode = en;
                        }
                    }
                }
                
            }
            
        }
        else
        {
            TreePath selectedPath = tree.getClosestPathForLocation(e.getX(), e.getY());
            for(int i = 0; i < editableModules.size(); i++) //search each module
            {
                ModuleNode mn = (ModuleNode)editableModules.get(i);
                if(new TreePath(mn.getPath()).equals(selectedPath))
                {
                    tree.setSelectionPath(selectedPath);
                    if(graphicEditor != null)graphicEditor.switchModuleView(mn);
                    return;
                }
            }
        }
        
    }
    
    public String getToolTipText()
    {
        return handler.getParseErrorMessage();
    }
    
    public ModelType getModelType()
    {
        return ModelType.valueOf(modelType.getUserObject().toString());
    }
    
    public String getParseText()
    {
        int i,j;
        String str = "";
        //Header
        str+="//Generated by the PRISM Graphic Model Editor\n";
        str+="\n";
        
        //Model Type
        String type = modelType.getUserObject().toString();
        str += type.toLowerCase() + "\n\n";
        
        //Constants
        if(constants.getChildCount() != 0)
        {
            str+="//Constants\n\n";
            for(i = 0; i < constants.getChildCount(); i++)
            {
                ConstantNode cn = (ConstantNode)constants.getChildAt(i);
                if(cn.isEditable())str+=cn.getParseText()+"\n";
            }
            str+="\n";
        }
        
        //Globals
        if(declarations.getChildCount() != 0)
        {
            str+="//Globals\n\n";
            for(i = 0; i < declarations.getChildCount(); i++)
            {
                DeclarationNode gn = (DeclarationNode)declarations.getChildAt(i);
                if(gn.isEditable())str+= gn.getParseText()+"\n";
            }
            str+="\n";
        }
        
        //Modules
        if(modules.getChildCount() != 0)
        {
            str+="//GUI Modules\n\n";
            for(i = 0; i < modules.getChildCount(); i++)
            {
                ModuleNode mn = (ModuleNode)modules.getChildAt(i);
                if(mn.isEditable())
                {
                    str+="module "+mn.getName()+"\n";
                    for(j = 0; j < mn.getChildCount(); j++)
                    {
                        DeclarationNode dn = (DeclarationNode)mn.getChildAt(j);
                        str+=TAB+dn.getParseText()+"\n";
                    }
                    
                    
                    ModuleModel aModuleModel = mn.getModuleModel();
                    String stateVar = ((StateVarNode)mn.getChildAt(0)).getName();
                    //now add the transition information
                    for(j = 0; j < aModuleModel.getNumStates(); j++)
                    {
                        State aState = aModuleModel.getState(j);
                        if(!aState.getCommentLabel().getString().equals(""))
                            str+=TAB+("//"+aState.getComment()+"\n");
                        for(int k = 0; k < aModuleModel.getNumTransitions(); k++)
                        {
                            Transition aTrans = aModuleModel.getTransition(k);
                            if(aTrans.getFrom() == aState)
                            {
                                if(!(aTrans instanceof ProbTransition || aTrans.getTo() instanceof Decision))// if not branched
                                {
                                    
                                    String sync = removeCarriages(aTrans.getSyncLabel().getString());
                                    String guard = removeCarriages(aTrans.getGuardLabel().getString());
                                    if(!guard.equals("")) guard = " & ("+guard+")";
                                    String assign = removeCarriages(aTrans.getAssignmentLabel().getString());
                                    if(!assign.equals("")) assign = " & "+assign+"";
                                    String prob = removeCarriages(aTrans.getProbabilityLabel().getString());
                                    int to = aModuleModel.getStateIndex(aTrans.getTo());
                                    if(prob.equals("") || prob == null)
                                    {
                                        str+=TAB+("["+sync+"]"+ "("+stateVar+"="+j+") "+guard+" -> ("+stateVar+"'="+to+")"+assign+";"+"\n");
                                    }
                                    else
                                    {
                                        str+=TAB+("["+sync+"]"+ "("+stateVar+"="+j+") "+guard+" -> "+ prob +" : ("+stateVar+"'="+to+")"+assign+";"+"\n");
                                    }
                                }
                                else if(aTrans.getTo() instanceof Decision) // if branched
                                {
                                    String sync = removeCarriages(aTrans.getSyncLabel().getString());
                                    String guard = removeCarriages(aTrans.getGuardLabel().getString());
                                    if(!guard.equals("")) guard = " & ("+guard+")";
                                    str+=(TAB+"["+sync+"] ("+stateVar+"="+j+") "+guard+" -> ");
                                    Decision dec = (Decision)(aTrans.getTo());
                                    boolean firstDone = false;
                                    for(int l = 0; l < aModuleModel.getNumTransitions(); l++)
                                    {
                                        Transition branch = aModuleModel.getTransition(l);
                                        if(branch.getFrom() == dec)
                                        {
                                            ProbTransition pTran = (ProbTransition)branch;
                                            String prob = pTran.getProbabilityLabel().getString();
                                            int to = aModuleModel.getStateIndex(pTran.getTo());
                                            String assign = removeCarriages(pTran.getAssignmentLabel().getString());
                                            if(!assign.equals("")) assign = " & "+assign+"";
                                            if(firstDone)str+=("+ ");
                                            firstDone = true;
                                            str+=(prob+" : "+"("+stateVar+"'="+to+")"+assign+" ");
                                        }
                                    }
                                    str+=(";\n");
                                }
                            }
                        }
                    }
                    
                    str+="\n";
                    str+="endmodule\n\n";
                }
            }
            str+="\n";
            
        }
        //System.out.println("parsed model = "+str);
        return str;
    }
    public static final String TAB = "	";
    
    public ArrayList getEditableConstantNames()
    {
        ArrayList names = new ArrayList();
        for(int i = 0; i < editableConstants.size(); i++)
        {
            DeclarationNode dn = (DeclarationNode)editableConstants.get(i);
            names.add(dn.getName());
        }
        return names;
    }
    
    public ArrayList getEditableConstantValues()
    {
        ArrayList values = new ArrayList();
        for(int i = 0; i < editableConstants.size(); i++)
        {
            ConstantNode cn = (ConstantNode)editableConstants.get(i);
            if(cn.getValue() != null)
            {
                if(!cn.getValue().toString().equals(""))
                {
                    values.add(cn.getValue().toString());
                }
                else
                    values.add(null);
            }
            else values.add(null);
        }
        return values;
    }
    
    public ArrayList<Type> getEditableConstantTypes()
    {
        ArrayList<Type> types = new ArrayList<Type>();
        for(int i = 0; i < editableConstants.size(); i++)
        {
            Object node = editableConstants.get(i);
            if(node instanceof BoolConstantNode)
            {
                types.add(TypeBool.getInstance());
            }
            else if(node instanceof IntegerConstantNode)
            {
                types.add(TypeInt.getInstance());
            }
            else if(node instanceof DoubleConstantNode)
            {
                types.add(TypeDouble.getInstance());
            }
            else types.add(null);
        }
        return types;
    }
    
    public ArrayList getEditableGlobalNames()
    {
        ArrayList names = new ArrayList();
        for(int i = 0; i < editableDeclarations.size(); i++)
        {
            DeclarationNode dn = (DeclarationNode)editableDeclarations.get(i);
            names.add(dn.getName());
        }
        return names;
    }
    
    public ArrayList getEditableGlobalMins()
    {
        ArrayList mins = new ArrayList();
        for(int i = 0; i < editableDeclarations.size(); i++)
        {
            Object node = editableDeclarations.get(i);
            if(node instanceof GlobalNode)
            {
                GlobalNode gn = (GlobalNode)node;
                mins.add(gn.getMin().toString());
            }
            else
                mins.add(null);
        }
        return mins;
    }
    
    public ArrayList getEditableGlobalMaxs()
    {
        ArrayList maxs = new ArrayList();
        for(int i = 0; i < editableDeclarations.size(); i++)
        {
            Object node = editableDeclarations.get(i);
            if(node instanceof GlobalNode)
            {
                GlobalNode gn = (GlobalNode)node;
                maxs.add(gn.getMax().toString());
            }
            else
                maxs.add(null);
            
        }
        return maxs;
    }
    
    public ArrayList getEditableGlobalInits()
    {
        ArrayList inits = new ArrayList();
        for(int i = 0; i < editableDeclarations.size(); i++)
        {
            Object node = editableDeclarations.get(i);
            if(node instanceof GlobalNode)
            {
                GlobalNode gn = (GlobalNode)node;
                inits.add(gn.getInitial().toString());
            }
            else if(node instanceof GlobalBoolNode)
            {
                GlobalBoolNode gbn = (GlobalBoolNode)node;
                inits.add(gbn.getInitial().toString());
            }
        }
        return inits;
    }
    
    public ArrayList<Type> getEditableGlobalTypes()
    {
        ArrayList<Type> types = new ArrayList<Type>();
        for(int i = 0; i < editableDeclarations.size(); i++)
        {
            Object node = editableDeclarations.get(i);
            if(node instanceof GlobalBoolNode)
            {
                types.add(TypeBool.getInstance());
            }
            else if(node instanceof GlobalNode)
            {
                types.add(TypeInt.getInstance());
            }
            else types.add(null);
        }
        return types;
    }
    
    public ArrayList getVariableNames(ModuleNode m)
    {
        ArrayList names = new ArrayList();
        for(int i = 0; i < m.getChildCount(); i++)
        {
            DeclarationNode vn = (DeclarationNode)m.getChildAt(i);
            if(!(vn instanceof StateVarNode))
            {
                names.add(vn.getName());
            }
        }
        return names;
    }
    
    public ArrayList<Type> getVariableTypes(ModuleNode m)
    {
        ArrayList<Type> types = new ArrayList<Type>();
        for(int i = 0; i < m.getChildCount(); i++)
        {
            DeclarationNode dn = (DeclarationNode)m.getChildAt(i);
            if(!(dn instanceof StateVarNode))
            {
                if(dn instanceof BoolNode)
                    types.add(TypeBool.getInstance());
                else if(dn instanceof VarNode)
                    types.add(TypeInt.getInstance());
                else
                    types.add(null);
            }
        }
        return types;
    }
    
    public ArrayList getVariableMins(ModuleNode m)
    {
        ArrayList mins = new ArrayList();
        for(int i = 0; i < m.getChildCount(); i++)
        {
            DeclarationNode dn = (DeclarationNode)m.getChildAt(i);
            if(!(dn instanceof StateVarNode))
            {
                if(dn instanceof BoolNode)
                    mins.add(null);
                else if(dn instanceof VarNode)
                {
                    VarNode vn = (VarNode)dn;
                    String s = vn.getMin().toString();
                    mins.add(s);
                }
                else
                    mins.add(null);
            }
        }
        return mins;
    }
    
    public ArrayList getVariableMaxs(ModuleNode m)
    {
        ArrayList maxs = new ArrayList();
        for(int i = 0; i < m.getChildCount(); i++)
        {
            DeclarationNode dn = (DeclarationNode)m.getChildAt(i);
            if(!(dn instanceof StateVarNode))
            {
                if(dn instanceof BoolNode)
                    maxs.add(null);
                else if(dn instanceof VarNode)
                {
                    VarNode vn = (VarNode)dn;
                    String s = vn.getMax().toString();
                    maxs.add(s);
                }
                else
                    maxs.add(null);
            }
        }
        return maxs;
    }
    
    public ArrayList getVariableInits(ModuleNode m)
    {
        ArrayList inits = new ArrayList();
        for(int i = 0; i < m.getChildCount(); i++)
        {
            DeclarationNode dn = (DeclarationNode)m.getChildAt(i);
            if(!(dn instanceof StateVarNode))
            {
                if(dn instanceof BoolNode)
                {
                    BoolNode bn = (BoolNode)dn;
                    String s = bn.getInitial().toString();
                    inits.add(s);
                }
                else if(dn instanceof VarNode)
                {
                    VarNode vn = (VarNode)dn;
                    String s = vn.getInitial().toString();
                    inits.add(s);
                }
                else
                    inits.add(null);
            }
        }
        return inits;
    }
    
    public void updateTooltip()
    {
        tree.setToolTipText(handler.getParseErrorMessage());
    }
    
    
    
    
    
    
    
    //Node Data Structure Classes
    
    interface PrismTreeNode
    {
        public boolean isEditable();
    }
    
    class ModelRootNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        public ModelRootNode()
        {
            super("", true);
        }
        
        public boolean isEditable()
        {
            return false;
        }
        
    }
    
    class ModuleCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        public ModuleCollectionNode()
        {
            super("Modules", true);
            super.setAllowsChildren(true);
        }
        
        public void addModule(ModuleNode mod)
        {
            add(mod);
        }
        
        public void removeModule(ModuleNode mod)
        {
            remove(mod);
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
    }
    
    class DeclarationCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        public DeclarationCollectionNode()
        {
            super("Global Variables", true);
            super.setAllowsChildren(true);
        }
        
        public void addDeclaration(DeclarationNode dec)
        {
            add(dec);
        }
        
        public void removeDeclaration(DeclarationNode dec)
        {
            remove(dec);
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
    }
    
    class ConstantCollectionNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        public ConstantCollectionNode()
        {
            super("Constants", true);
        }
        
        public void addConstant(ConstantNode n)
        {
            add(n);
        }
        
        public void removeConstant(ConstantNode n)
        {
            remove(n);
        }
        
        public boolean isEditable()
        {
            return editable;
        }
    }
    
    public class ModuleNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        private boolean editable;
        private ModuleModel moduleModel;
        
        public ModuleNode(String moduleName, boolean editable)
        {
            super(moduleName, true);
            moduleModel = null;
            this.editable = editable;
        }
        
        public void addVariable(VarNode var)
        {
            add(var);
        }
        
        public void removeVariable(VarNode var)
        {
            remove(var);
        }
        
        public void setName(String str)
        {
            setUserObject(str);
        }
        
        public String getName()
        {
            return (String)getUserObject();
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
        public void setEditable(boolean b)
        {
            editable = b;
        }
        
        public void setModel(ModuleModel n)
        {
            moduleModel = n;
        }
        
        public ModuleModel getModuleModel()
        {
            return moduleModel;
        }
        
        public void childrenChanged()
        {
            theModel.nodeChanged(this);
            theModel.nodeStructureChanged(this);
        }
        
        public boolean isLeaf()
        {
            return false;
        }
        
    }
    //Editor for ModuleNode
    class ModuleEditor extends JTextField implements TreeCellEditor
    {
        String name;
        Vector listeners = new Vector();
        private static final int minWidth = 64;
        
        public ModuleEditor()
        {
            super("");
            addActionListener(new ActionListener()
            {
                public void actionPerformed(ActionEvent as)
                {
                    if(stopCellEditing())
                        fireEditingStopped();
                }
            });
        }
        
        public void cancelCellEditing()
        {
            setText("");
        }
        
        public boolean stopCellEditing()
        {
        	 Expression exp;
                String str = getText();
                try  {
                    exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str);
                }
                catch (PrismException e) {
                	return false;
                }
                    if(exp instanceof ExpressionIdent)
                    {
                        name = str;
                        return true;
                    }
                    else
                    {
                        return false;
                    }
        }
        
        public Object getCellEditorValue()
        {
            return name;
        }
        
        public boolean isCellEditable(EventObject eo)
        {
            if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                return true;
            }
            return false;
        }
        
        public boolean shouldSelectCell(EventObject eo)
        {
            return true;
        }
        
        public void removeCellEditroLIstner(CellEditorListener cel)
        {
            listeners.removeElement(cel);
        }
        
        protected void fireEditingStopped()
        {
            if(listeners.size() > 0)
            {
                ChangeEvent ce = new ChangeEvent(this);
                for(int i = listeners.size()-1; i >=0; i--)
                {
                    ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce);
                }
                
            }
        }
        //make sure the JTree gives the editor enough space
        public void setBounds(Rectangle r)
        {
            r.width = Math.max(minWidth, r.width);
            super.setBounds(r);
        }
        
        public void setBounds(int x, int y, int w, int h)
        {
            w = Math.max(minWidth, w);
            super.setBounds(x,y,w,h);
        }
        
        public void addCellEditorListener(CellEditorListener l)
        {
            listeners.addElement(l);
        }
        
        public void removeCellEditorListener(CellEditorListener l)
        {
            listeners.removeElement(l);
        }
        
        public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
        {
            return this;
        }
        
        //same listener and bounds methods as above
    }
    
    public static final int LOCAL_INTEGER	= 0;
    public static final int LOCAL_BOOL	   = 1;
    public static final int GLOBAL_INTEGER   = 2;
    public static final int GLOBAL_BOOL	  = 3;
    public static final int CONST_INTEGER	= 4;
    public static final int CONST_BOOL	   = 5;
    public static final int CONST_DOUBLE	 = 6;
    
    
    abstract class DeclarationNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        private boolean editable;
        private int type;
        
        public DeclarationNode(int type, String name, boolean editable)
        {
            super(name, true);
            this.editable = editable;
            this.type = type;
        }
        
        public boolean getAllowsChildren()
        {
            return true;
        }
        
        public boolean isLeaf()
        {
            return false;
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
        public String getName()
        {
            return (String)getUserObject();
        }
        
        public void setName(String str)
        {
            setUserObject(str);
        }
        
        public String toString()
        {
            String name = getName();
            switch(type)
            {
                case LOCAL_INTEGER: return name;
                case GLOBAL_INTEGER:
                case CONST_INTEGER: return name+" : int";
                case LOCAL_BOOL:
                case GLOBAL_BOOL:
                case CONST_BOOL: return name+" : bool";
                case CONST_DOUBLE: return name+" : double";
                default: return "";
            }
        }
        
        public abstract String getParseText();
    }
    //Editor for DeclarationNode
    class DeclarationEditor extends JTextField implements TreeCellEditor
    {
        String name;
        Vector listeners = new Vector();
        private static final int minWidth = 64;
        
        public DeclarationEditor()
        {
            super("");
            addActionListener(new ActionListener()
            {
                public void actionPerformed(ActionEvent as)
                {
                    if(stopCellEditing())
                        fireEditingStopped();
                }
            });
        }
        
        public void cancelCellEditing()
        {
            setText("");
        }
        
        public boolean stopCellEditing()
        {
       	 Expression exp;
         String str = getText();
         try  {
             exp = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str);
         }
         catch (PrismException e) {
         	return false;
         }
             if(exp instanceof ExpressionIdent)
             {
                 name = str;
                 return true;
             }
             else
             {
                 return false;
             }
        }
        
        public Object getCellEditorValue()
        {
            return name;
        }
        
        public boolean isCellEditable(EventObject eo)
        {
            if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                return true;
            }
            return false;
        }
        
        public boolean shouldSelectCell(EventObject eo)
        {
            return true;
        }
        
        protected void fireEditingStopped()
        {
            if(listeners.size() > 0)
            {
                ChangeEvent ce = new ChangeEvent(this);
                for(int i = listeners.size()-1; i >=0; i--)
                {
                    ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce);
                }
                
            }
        }
        //make sure the JTree gives the editor enough space
        public void setBounds(Rectangle r)
        {
            r.width = Math.max(minWidth, r.width);
            super.setBounds(r);
        }
        
        public void setBounds(int x, int y, int w, int h)
        {
            w = Math.max(minWidth, w);
            super.setBounds(x,y,w,h);
        }
        
        public void addCellEditorListener(CellEditorListener l)
        {
            listeners.addElement(l);
        }
        
        public void removeCellEditorListener(CellEditorListener l)
        {
            listeners.addElement(l);
        }
        
        public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
        {
            return this;
        }
        
    }
    
    class VarNode extends DeclarationNode
    {
        
        public VarNode(String name, Expression init, Expression min, Expression max, boolean editable)
        {
            super(LOCAL_INTEGER, name, editable);
            super.add(new ExpressionNode("min: ", min, editable));
            super.add(new ExpressionNode("max: ", max, editable));
            super.add(new ExpressionNode("init: ", init, editable));
        }
        
        public VarNode(String name, String init, String min, String max, boolean editable)
        {
            super(LOCAL_INTEGER, name, editable);
            try
            {
                Expression e_init = handler.getGUIPlugin().getPrism().parseSingleExpressionString(init);
                Expression e_min = handler.getGUIPlugin().getPrism().parseSingleExpressionString(min);
                Expression e_max = handler.getGUIPlugin().getPrism().parseSingleExpressionString(max);
                super.add(new ExpressionNode("min: ", e_min, editable));
                super.add(new ExpressionNode("max: ", e_max, editable));
                super.add(new ExpressionNode("init: ", e_init, editable));
            }
            catch(Exception e)
            {}
        }
        
        public void setInitial(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(2);
            n.setUserObject(e);
            theModel.nodeChanged(getChildAt(2));
        }
        
        public Expression getInitial()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(2);
            return n.getValue();
        }
        
        public void setMin(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
            theModel.nodeChanged(getChildAt(0));
        }
        
        public Expression getMin()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public void setMax(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(1);
            n.setUserObject(e);
            theModel.nodeChanged(getChildAt(1));
        }
        
        public Expression getMax()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(1);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = getName()+" : ["+getMin()+".."+getMax()+"] init "+getInitial()+";";
            return str;
        }
        
    }
    
    public class StateVarNode extends VarNode
    {
        ModuleNode mn;
        public StateVarNode(ModuleNode mn) throws prism.PrismException
        {
            super("statevariable", "0", "0", "0", false);
            this.mn = mn;
        }
        
        public String getName()
        {
            return mn.getName()+"_s";
        }
    }
    
    class BoolNode extends DeclarationNode
    {
        public BoolNode(String name, Expression init, boolean editable)
        {
            super(LOCAL_BOOL, name, editable);
            super.add(new ExpressionNode("init: ", init, editable));
        }
        
        public void setInitial(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getInitial()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = getName()+" : bool init "+getInitial()+";";
            return str;
        }
        
    }
    
    class GlobalNode extends DeclarationNode
    {
        
        public GlobalNode(String name, Expression init, Expression min, Expression max, boolean editable)
        {
            super(GLOBAL_INTEGER, name, editable);
            super.add(new ExpressionNode("min: ", min, editable));
            super.add(new ExpressionNode("max: ", max, editable));
            super.add(new ExpressionNode("init: ", init, editable));
        }
        
        public void setInitial(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(2);
            n.setUserObject(e);
        }
        
        public Expression getInitial()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(2);
            return n.getValue();
        }
        
        public void setMin(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getMin()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public void setMax(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(1);
            n.setUserObject(e);
        }
        
        public Expression getMax()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(1);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = "global "+getName()+" : ["+getMin()+".."+getMax()+"] init "+getInitial()+";";
            return str;
        }
        
    }
    
    class GlobalBoolNode extends DeclarationNode
    {
        public GlobalBoolNode(String name, Expression init, boolean editable)
        {
            super(GLOBAL_BOOL, name, editable);
            super.add(new ExpressionNode("init: ", init, editable));
        }
        
        public void setInitial(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getInitial()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = "global "+getName()+" : bool init "+getInitial()+";";
            return str;
        }
        
    }
    
    abstract class ConstantNode extends DeclarationNode
    {
        public ConstantNode(int type, String name, boolean editable)
        {
            super(type, name, editable);
        }
        
        public abstract void setValue(Expression e);
        
        public abstract Expression getValue();
        
        public boolean equals(Object obj)
        {
            if(obj instanceof ConstantNode)
            {
                ConstantNode other = (ConstantNode)obj;
                if(!other.getName().equals(getName())) return false;
                else return true;  //can only compare the equality of the names
            }
            else return false;
        }
        
        public abstract String getParseText();
        
    }
    
    class IntegerConstantNode extends ConstantNode
    {
        public IntegerConstantNode(String name, Expression value, boolean editable)
        {
            super(CONST_INTEGER, name, editable);
            super.add(new ExpressionNode("value: ", value, editable));
        }
        
        public void setValue(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getValue()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = "const int "+getName();
            if(getValue() != null)
            {
                str+=" = "+getValue()+";";
            }
            else
            {
                str+=";";
            }
            return str;
        }
        
    }
    
    class DoubleConstantNode extends ConstantNode
    {
        public DoubleConstantNode(String name, Expression value, boolean editable)
        {
            super(CONST_DOUBLE, name, editable);
            super.add(new ExpressionNode("value: ", value, editable));
        }
        
        public void setValue(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getValue()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = "const double "+getName();
            if(getValue() != null)
            {
                str+=" = "+getValue()+";";
            }
            else
            {
                str+=";";
            }
            return str;
        }
        
    }
    
    class BoolConstantNode extends ConstantNode
    {
        public BoolConstantNode(String name, Expression value, boolean editable)
        {
            super(CONST_BOOL, name, editable);
            super.add(new ExpressionNode("value: ", value, editable));
        }
        
        public void setValue(Expression e)
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            n.setUserObject(e);
        }
        
        public Expression getValue()
        {
            ExpressionNode n = (ExpressionNode)getChildAt(0);
            return n.getValue();
        }
        
        public String getParseText()
        {
            String str = "const bool "+getName();
            if(getValue() != null)
            {
                str+=" = "+getValue()+";";
            }
            else
            {
                str+=";";
            }
            return str;
        }
        
    }
    
    
    abstract class ValueNode extends DefaultMutableTreeNode implements PrismTreeNode
    {
        private String tag;
        
        public ValueNode(String tag, Object value)
        {
            super(value);
            this.tag = tag;
        }
        
        public String toString()
        {
            if(getUserObject() == null) return tag+"?";
            else return tag+getUserObject().toString();
        }
        
        public abstract boolean isEditable();
        
        public boolean isLeaf()
        {
            return true;
        }
        
        public void setUserObject(Object obj)
        {
            super.setUserObject(obj);
        }
    }
    
    class StringNode extends ValueNode
    {
        private boolean editable;
        
        public StringNode(String tag, String value, boolean editable)
        {
            super(tag, value);
            this.editable = editable;
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
        public String getValue()
        {
            return (String)getUserObject();
        }
        
    }
    
    class ExpressionNode extends ValueNode
    {
        private boolean editable;
        
        public ExpressionNode(String tag, Expression value, boolean editable)
        {
            super(tag, value);
            this.editable = editable;
        }
        
        public boolean isEditable()
        {
            return editable;
        }
        
        public Expression getValue()
        {
            return (Expression)getUserObject();
        }
        
        public void setValue(Expression value)
        {
            super.setUserObject(value);
        }
        
    }
        /*
        class ExpressionEditor extends javax.swing.DefaultCellEditor
        {
                Expression exp;
                int minWidth = 100;
         
                public ExpressionEditor()
                {
                        super(new JTextField());
                }
         
                public Component getComponent()
                {
                        return editorComponent;
                }
         
                public boolean stopCellEditing()
                {
                        String str = ((JTextField)editorComponent).getText();
         
                        try
                        {
                                Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str);
                                exp = s;
                        }
                        catch(Exception e)
                        {
                                handler.getGUIPlugin().message("Error: Syntax Error");
                                super.fireEditingStopped();
                                return true;
                        }
                        super.fireEditingStopped();
                        return true;
         
                }
         
                public void setBounds(Rectangle r)
                {
                        r.width = Math.max(minWidth, r.width);
                        getComponent().setBounds(r);
                        tree.repaint();
                }
         
                public void setBounds(int x, int y, int w, int h)
                {
                        w = Math.max(minWidth, w);
                        getComponent().setBounds(x,y,w,h);
                        tree.repaint();
                }
        }*/
    
    //Cell edit for ExpressionNode
    class ExpressionEditor extends JTextField implements TreeCellEditor
    {
        Expression exp;
        Vector listeners = new Vector();
        private static final int minWidth = 64;
        
        public ExpressionEditor()
        {
            super("");
            addActionListener(new ActionListener()
            {
                public void actionPerformed(ActionEvent as)
                {
                    if(stopCellEditing())
                        fireEditingStopped();
                }
            });
        }
        
        public void cancelCellEditing()
        {
            setText("");
        }
        
        public boolean stopCellEditing()
        {
            String str = getText();
            
            try
            {
                Expression s = handler.getGUIPlugin().getPrism().parseSingleExpressionString(str);
                exp = s;
            }
            catch(Exception e)
            {
                handler.getGUIPlugin().message("Error: Syntax Error");
                return true;
            }
            return true;
            
        }
        
        public Object getCellEditorValue()
        {
            return exp;
        }
        
        public boolean isCellEditable(EventObject eo)
        {
            if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                MouseEvent me = (MouseEvent)eo;
                if(me.getClickCount() >= 2)
                {
                    return true;
                }
            }
            return false;
        }
        
        public boolean shouldSelectCell(EventObject eo)
        {
            if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                MouseEvent me = (MouseEvent)eo;
                if(me.getClickCount() >= 2)
                {
                    return true;
                }
            }
            return false;
        }
        
        protected void fireEditingStopped()
        {
            if(listeners.size() > 0)
            {
                ChangeEvent ce = new ChangeEvent(this);
                for(int i = listeners.size()-1; i >=0; i--)
                {
                    ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce);
                }
                
            }
        }
        //make sure the JTree gives the editor enough space
        public void setBounds(Rectangle r)
        {
            r.width = Math.max(minWidth, r.width);
            super.setBounds(r);
            tree.repaint();
        }
        
        public void setBounds(int x, int y, int w, int h)
        {
            w = Math.max(minWidth, w);
            super.setBounds(x,y,w,h);
            tree.repaint();
        }
        
        public void addCellEditorListener(CellEditorListener l)
        {
            listeners.addElement(l);
        }
        
        public void removeCellEditorListener(CellEditorListener l)
        {
            listeners.addElement(l);
        }
        
        public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
        {
            return this;
        }
        
    }
    
    class ModelTypeNode extends StringNode
    {
        public ModelTypeNode(String init, boolean editable)
        {
            super("Type: ", init, editable);
        }
        
        public void setModelType(ModelType type)
        {
            setUserObject(type.toString());
            switch (type) {
            case MDP: non.setSelected(true); break;
            case DTMC: pro.setSelected(true); break;
            case CTMC: sto.setSelected(true); break;
            }
            theModel.nodeChanged(this);
        }
        
        public void setUserObject(Object obj)
        {
            super.setUserObject(obj);
            //System.out.println("setting model type user object "+obj);
            
        }
    }
    //Cell Editor for ModelTypeNode
    class ModelTypeEditor extends JComboBox implements TreeCellEditor
    {
        String value;
        Vector listeners = new Vector();
        private static final int minWidth = 36;
        Object[] list;
        
        public ModelTypeEditor(Object[] list)
        {
            super(list);
            setFont(tree.getFont());
            setBackground(Color.white);
            setForeground(Color.blue);
            
            this.list = list;
            setEditable(false);//why???
            value = list[0].toString();
            
            addActionListener(new ActionListener()
            {
                public void actionPerformed(ActionEvent e)
                {
                    if(stopCellEditing())
                        fireEditingStopped();
                }
            });
        }
        
        public void setSelectedType(String str)
        {
            for(int i = 0; i < list.length; i++)
            {
                String cur = (String)list[i];
                if(cur.equals(str))
                {
                    super.setSelectedIndex(i);
                    break;
                }
            }
        }
        
        public void cancelCellEditing()
        {}
        
        public boolean stopCellEditing()
        {
            try
            {
                value = (String)getSelectedItem();
                if(value == null)
                {
                    value = (String)getItemAt(0);
                }
                return true;
                
            }
            catch(Exception e)
            {
                return false;
            }
        }
        
        public Object getCellEditorValue()
        {
            return value;
        }
        
        public boolean isCellEditable(EventObject eo)
        {
            if((eo == null) || ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                MouseEvent me = (MouseEvent)eo;
                if(me.getClickCount() >= 2)
                {
                    return true;
                }
            }
            return false;
        }
        
        public boolean shouldSelectCell(EventObject eo)
        {
            if((eo == null) | ((eo instanceof MouseEvent) && (((MouseEvent)eo).isMetaDown())))
            {
                MouseEvent me = (MouseEvent)eo;
                if(me.getClickCount() >= 2)
                {
                    return true;
                }
            }
            return false;
        }
        
        public void addCellEditorListener(CellEditorListener cel)
        {
            listeners.addElement(cel);
        }
        
        public void removeCellEditorListener(CellEditorListener cel)
        {
            listeners.removeElement(cel);
        }
        
        protected void fireEditingStopped()
        {
            if(listeners.size() > 0)
            {
                ChangeEvent ce = new ChangeEvent(this);
                for(int i = listeners.size()-1; i >=0; i--)
                {
                    ((CellEditorListener)listeners.elementAt(i)).editingStopped(ce);
                }
                
            }
        }
        
        public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
        {
            return this;
        }
        
/*
                //make sure the JTree gives the editor enough space
                public void setBounds(Rectangle r)
                {
                                r.width = Math.max(minWidth, r.width);
                                super.setBounds(r);
                }
 
                public void setBounds(int x, int y, int w, int h)
                {
                                w = Math.max(minWidth, w);
                                super.setBounds(x,y,w,h);
                }*/
        
    }
    
    
    //Node Renderer
    class PrismNodeRenderer extends DefaultTreeCellRenderer
    {
        ImageIcon VAR = GUIPrism.getIconFromImage("smallVariable.png");
        ImageIcon MOD = GUIPrism.getIconFromImage("smallModule.png");
        //ImageIcon EXP = GUIPrism.getIconFromImage("smallExpression.png");
        ImageIcon VAL = GUIPrism.getIconFromImage("smallValue.png");
        ImageIcon GOOD = GUIPrism.getIconFromImage("smallTick.png");
        ImageIcon BAD = GUIPrism.getIconFromImage("smallCross.png");
        ImageIcon OUT_OF_SYNCH = GUIPrism.getIconFromImage("smallFilePrism.png");
        ImageIcon CLOCK = GUIPrism.getIconFromImage("smallClockAnim1.png");
        
        public Component getTreeCellRendererComponent(JTree tree, Object value, boolean selected, boolean expanded, boolean leaf, int row, boolean hasFocus)
        {
            super.getTreeCellRendererComponent(tree,value,selected,expanded,leaf,row,hasFocus);
            PrismTreeNode node = (PrismTreeNode)value;
            
            if(node == root)
            {
                if (isParsing)
                {
                    setIcon(animIcon);
                } else
                {
                    switch(parseSynchState)
                    {
                        case TREE_SYNCHRONIZED_GOOD: setIcon(GOOD);break;
                        case TREE_SYNCHRONIZED_BAD: setIcon(BAD);break;
                        case TREE_NOT_SYNCHRONIZED: setIcon(OUT_OF_SYNCH);break;
                    }
                }
            }
            else if(node instanceof VarNode)
            {
                setIcon(VAR);
            }
            else if(node instanceof BoolNode)
            {
                setIcon(VAR);
            }
            else if(node instanceof DeclarationNode)
            {
                setIcon(VAR);
            }
            else if(node instanceof ModuleNode)
            {
                setIcon(MOD);
            }
            else if(node instanceof ValueNode)
            {
                //if(node instanceof ExpressionNode)
                //{
                    //setIcon(EXP);
                //}
                //else
                {
                    setIcon(VAL);
                }
            }
            else if(node instanceof ModuleCollectionNode || node instanceof DeclarationCollectionNode || node instanceof ConstantCollectionNode)
            {
                setIcon(this.getDefaultClosedIcon());
            }
            if(node.isEditable())
            {
                setForeground(Color.blue);
            }
            else setForeground(Color.black);
            
            return this;
        }
    }
    
    class ModelTreeCellEditor extends DefaultTreeCellEditor
    {
        ModelTypeEditor modelTypeEditor;
        ExpressionEditor expressionEditor;
        ModuleEditor moduleEditor;
        DeclarationEditor declarationEditor;
        
        String[] types = new String[]
        {"Non-deterministic", "Probabilistic", "Stochastic"};
        
        public ModelTreeCellEditor(JTree tree, PrismNodeRenderer renderer)
        {
            super(tree, renderer);
            modelTypeEditor = new ModelTypeEditor(types);
            expressionEditor = new ExpressionEditor();
            moduleEditor = new ModuleEditor();
            declarationEditor = new DeclarationEditor();
            realEditor = declarationEditor;
        }
        
        public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
        {
            if(value instanceof ExpressionNode)
            {
                realEditor = expressionEditor;
                //((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString());
            }
            else if(value instanceof ModelTypeNode)
            {
                realEditor = modelTypeEditor;
                modelTypeEditor.setSelectedType(((ModelTypeNode)value).getValue());
                //tag = "Type: ";
            }
            else if(value instanceof ModuleNode)
            {
                realEditor = moduleEditor;
                moduleEditor.setText(((ModuleNode)value).getName());
            }
            else if(value instanceof DeclarationNode)
            {
                realEditor = declarationEditor;
                declarationEditor.setText(((DeclarationNode)value).getName());
            }
            return super.getTreeCellEditorComponent(tree, value, isSelected, expanded, leaf, row);
        }
        
        public void addCellEditorListener(CellEditorListener l)
        {
            
            modelTypeEditor.addCellEditorListener(l);
            expressionEditor.addCellEditorListener(l);
            
            moduleEditor.addCellEditorListener(l);
            
            declarationEditor.addCellEditorListener(l);
            super.addCellEditorListener(l);
        }
        
        public void removeCellEditorListener(CellEditorListener l)
        {
            modelTypeEditor.removeCellEditorListener(l);
            expressionEditor.removeCellEditorListener(l);
            
            moduleEditor.removeCellEditorListener(l);
            
            declarationEditor.removeCellEditorListener(l);
            super.removeCellEditorListener(l);
        }
    }
        /*
        class ModelTreeCellEditor_n implements TreeCellEditor
        {
                ModelTypeEditor modelTypeEditor;
                ExpressionEditor expressionEditor;
                ModuleEditor moduleEditor;
                DeclarationEditor declarationEditor;
         
                CellEditor currentEditor;
         
                DefaultTreeCellEditor ttt;
         
                String[] types = new String[]
                {"Non-deterministic", "Probabilistic", "Stochastic"};
         
                PrismNodeRenderer renderer;
         
                public ModelTreeCellEditor_n(PrismNodeRenderer renderer)
                {
                        this.renderer = renderer;
                        modelTypeEditor = new ModelTypeEditor(types);
                        expressionEditor = new ExpressionEditor();
                        moduleEditor = new ModuleEditor();
                        declarationEditor = new DeclarationEditor();
                        currentEditor = declarationEditor;
                }
         
         
         
                public Component getTreeCellEditorComponent(JTree tree, Object value, boolean isSelected, boolean expanded, boolean leaf, int row)
                {
                        String tag = "";
                        if(value instanceof ExpressionNode)
                        {
                                currentEditor = expressionEditor;
//				((JTextField)expressionEditor.getComponent()).setText(((ExpressionNode)value).getValue().toString());
                        }
                        else if(value instanceof ModelTypeNode)
                        {
                                currentEditor = modelTypeEditor;
                                modelTypeEditor.setSelectedType(((ModelTypeNode)value).getValue());
                                tag = "Type: ";
                        }
                        else if(value instanceof ModuleNode)
                        {
                                currentEditor = moduleEditor;
                                moduleEditor.setText(((ModuleNode)value).getName());
                        }
                        else if(value instanceof DeclarationNode)
                        {
                                currentEditor = declarationEditor;
                                declarationEditor.setText(((DeclarationNode)value).getName());
                        }
                        DefaultTreeCellRenderer c = (DefaultTreeCellRenderer)renderer.getTreeCellRendererComponent(tree, value, isSelected, expanded, leaf, row, true);
                        JPanel p = new JPanel();
                        p.setBackground(Color.white);
                        p.setLayout(new BorderLayout());
                        JLabel l = new JLabel(tag,c.getIcon(), JLabel.HORIZONTAL);
                        l.setBackground(Color.white);
                        l.setForeground(Color.blue);
                        l.setFont(tree.getFont());
                        p.add(l, BorderLayout.WEST);
                        if(currentEditor instanceof ExpressionEditor)
                        {
                                p.add(((ExpressionEditor)currentEditor).getComponent(), BorderLayout.CENTER);
                        }
                        else
                        {
                                p.add((Component)currentEditor, BorderLayout.CENTER);
                        }
                        return p;//(Component)currentEditor;
                }
         
                public Object getCellEditorValue()
                {
                        return currentEditor.getCellEditorValue();
         
                }
         
                public boolean isCellEditable(EventObject event)
                {
                        return true;
                        //return currentEditor.isCellEditable(event);
                }
         
                public boolean shouldSelectCell(EventObject event)
                {
                        return currentEditor.shouldSelectCell(event);
                }
         
                public boolean stopCellEditing()
                {
                        return currentEditor.stopCellEditing();
                }
         
                public void cancelCellEditing()
                {
                        currentEditor.cancelCellEditing();
                }
         
                public void addCellEditorListener(CellEditorListener l)
                {
         
                        modelTypeEditor.addCellEditorListener(l);
                        expressionEditor.addCellEditorListener(l);
         
                        moduleEditor.addCellEditorListener(l);
         
                        declarationEditor.addCellEditorListener(l);
                }
         
                public void removeCellEditorListener(CellEditorListener l)
                {
                        modelTypeEditor.removeCellEditorListener(l);
                        expressionEditor.removeCellEditorListener(l);
         
                        moduleEditor.removeCellEditorListener(l);
         
                        declarationEditor.removeCellEditorListener(l);
                }
         
        }
         
         */
    
    
    
    
    class IconThread extends Thread
    {
        int index;
        ImageIcon[] images;
        boolean canContinue = false;
        public IconThread(int index)
        {
            this.index = index;
            images = new ImageIcon[8];
            images[0] = GUIPrism.getIconFromImage("smallClockAnim1.png");
            images[1] = GUIPrism.getIconFromImage("smallClockAnim2.png");
            images[2] = GUIPrism.getIconFromImage("smallClockAnim3.png");
            images[3] = GUIPrism.getIconFromImage("smallClockAnim4.png");
            images[4] = GUIPrism.getIconFromImage("smallClockAnim5.png");
            images[5] = GUIPrism.getIconFromImage("smallClockAnim6.png");
            images[6] = GUIPrism.getIconFromImage("smallClockAnim7.png");
            images[7] = GUIPrism.getIconFromImage("smallClockAnim8.png");
        }
        public void run()
        {
            try
            {
                int counter = 0;
                while(!interrupted() && index>-1)
                {
                    counter++;
                    counter = counter%8;
                    animIcon = images[counter];
                    tree.repaint();
                    sleep(150);
                }
            }
            catch(InterruptedException e)
            {
            }
            canContinue = true;
        }
    }
    
    private static String removeCarriages(String line)
    {
        String lineBuffer = "";
        for(int i = 0; i < line.length(); i++)
        {
            char c = line.charAt(i);
            if(c!='\n') lineBuffer+=c;
            else lineBuffer+=" ";
        }
        return lineBuffer;
    }
}
